H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 28.32 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/FiniteMap.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ BR

mainModule FiniteMap

((foldFM_LE :: (Ratio Int -> b -> a -> a) -> a -> Ratio Int -> FiniteMap (Ratio Int) b -> a) :: (Ratio Int -> b -> a -> a) -> a -> Ratio Int -> FiniteMap (Ratio Int) b -> a)

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a)

instance (Eq a, Eq b) => Eq (FiniteMap b a) where

foldFM_LE :: Ord b => (b -> c -> a -> a) -> a -> b -> FiniteMap b c -> a

foldFM_LE

k z fr EmptyFM

foldFM_LE

k z fr (Branch key elt _ fm_l fm_r)

key <= fr

foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r

otherwise

foldFM_LE k z fr fm_l

module Maybe where

import qualified FiniteMap
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

mainModule FiniteMap

((foldFM_LE :: (Ratio Int -> b -> a -> a) -> a -> Ratio Int -> FiniteMap (Ratio Int) b -> a) :: (Ratio Int -> b -> a -> a) -> a -> Ratio Int -> FiniteMap (Ratio Int) b -> a)

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b)

instance (Eq a, Eq b) => Eq (FiniteMap b a) where

foldFM_LE :: Ord a => (a -> b -> c -> c) -> c -> a -> FiniteMap a b -> c

foldFM_LE

k z fr EmptyFM

foldFM_LE

k z fr (Branch key elt vw fm_l fm_r)

key <= fr

foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r

otherwise

foldFM_LE k z fr fm_l

module Maybe where

import qualified FiniteMap
import qualified Prelude

Cond Reductions:
The following Function with conditions

foldFM_LE k z fr EmptyFM = z

foldFM_LE k z fr (Branch key elt vw fm_l fm_r)

| key <= fr

= foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r

| otherwise

= foldFM_LE k z fr fm_l

is transformed to

foldFM_LE k z fr EmptyFM = foldFM_LE3 k z fr EmptyFM

foldFM_LE k z fr (Branch key elt vw fm_l fm_r) = foldFM_LE2 k z fr (Branch key elt vw fm_l fm_r)

foldFM_LE1 k z fr key elt vw fm_l fm_r True = foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r

foldFM_LE1 k z fr key elt vw fm_l fm_r False = foldFM_LE0 k z fr key elt vw fm_l fm_r otherwise

foldFM_LE0 k z fr key elt vw fm_l fm_r True = foldFM_LE k z fr fm_l

foldFM_LE2 k z fr (Branch key elt vw fm_l fm_r) = foldFM_LE1 k z fr key elt vw fm_l fm_r (key <= fr)

foldFM_LE3 k z fr EmptyFM = z

foldFM_LE3 wv ww wx wy = foldFM_LE2 wv ww wx wy

The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ Narrow

mainModule FiniteMap

(foldFM_LE :: (Ratio Int -> a -> b -> b) -> b -> Ratio Int -> FiniteMap (Ratio Int) a -> b)

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a)

instance (Eq a, Eq b) => Eq (FiniteMap a b) where

foldFM_LE :: Ord a => (a -> c -> b -> b) -> b -> a -> FiniteMap a c -> b

foldFM_LE	k z fr EmptyFM	=	foldFM_LE3 k z fr EmptyFM
foldFM_LE	k z fr (Branch key elt vw fm_l fm_r)	=	foldFM_LE2 k z fr (Branch key elt vw fm_l fm_r)

foldFM_LE0

k z fr key elt vw fm_l fm_r True

foldFM_LE k z fr fm_l

foldFM_LE1	k z fr key elt vw fm_l fm_r True	=	foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r
foldFM_LE1	k z fr key elt vw fm_l fm_r False	=	foldFM_LE0 k z fr key elt vw fm_l fm_r otherwise

foldFM_LE2

k z fr (Branch key elt vw fm_l fm_r)

foldFM_LE1 k z fr key elt vw fm_l fm_r (key <= fr)

foldFM_LE3	k z fr EmptyFM	=	z
foldFM_LE3	wv ww wx wy	=	foldFM_LE2 wv ww wx wy

module Maybe where

import qualified FiniteMap
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="foldFM_LE",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="foldFM_LE wz3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="foldFM_LE wz3 wz4",fontsize=16,color="grey",shape="box"];4 -> 5[label="",style="dashed", color="grey", weight=3];
5[label="foldFM_LE wz3 wz4 wz5",fontsize=16,color="grey",shape="box"];5 -> 6[label="",style="dashed", color="grey", weight=3];
6[label="foldFM_LE wz3 wz4 wz5 wz6",fontsize=16,color="burlywood",shape="triangle"];29634[label="wz6/EmptyFM",fontsize=10,color="white",style="solid",shape="box"];6 -> 29634[label="",style="solid", color="burlywood", weight=9];
29634 -> 7[label="",style="solid", color="burlywood", weight=3];
29635[label="wz6/Branch wz60 wz61 wz62 wz63 wz64",fontsize=10,color="white",style="solid",shape="box"];6 -> 29635[label="",style="solid", color="burlywood", weight=9];
29635 -> 8[label="",style="solid", color="burlywood", weight=3];
7[label="foldFM_LE wz3 wz4 wz5 EmptyFM",fontsize=16,color="black",shape="box"];7 -> 9[label="",style="solid", color="black", weight=3];
8[label="foldFM_LE wz3 wz4 wz5 (Branch wz60 wz61 wz62 wz63 wz64)",fontsize=16,color="black",shape="box"];8 -> 10[label="",style="solid", color="black", weight=3];
9[label="foldFM_LE3 wz3 wz4 wz5 EmptyFM",fontsize=16,color="black",shape="box"];9 -> 11[label="",style="solid", color="black", weight=3];
10[label="foldFM_LE2 wz3 wz4 wz5 (Branch wz60 wz61 wz62 wz63 wz64)",fontsize=16,color="black",shape="box"];10 -> 12[label="",style="solid", color="black", weight=3];
11[label="wz4",fontsize=16,color="green",shape="box"];12 -> 9824[label="",style="dashed", color="red", weight=0];
12[label="foldFM_LE1 wz3 wz4 wz5 wz60 wz61 wz62 wz63 wz64 (wz60 <= wz5)",fontsize=16,color="magenta"];12 -> 9825[label="",style="dashed", color="magenta", weight=3];
12 -> 9826[label="",style="dashed", color="magenta", weight=3];
12 -> 9827[label="",style="dashed", color="magenta", weight=3];
12 -> 9828[label="",style="dashed", color="magenta", weight=3];
12 -> 9829[label="",style="dashed", color="magenta", weight=3];
12 -> 9830[label="",style="dashed", color="magenta", weight=3];
12 -> 9831[label="",style="dashed", color="magenta", weight=3];
12 -> 9832[label="",style="dashed", color="magenta", weight=3];
12 -> 9833[label="",style="dashed", color="magenta", weight=3];
9825[label="wz3",fontsize=16,color="green",shape="box"];9826[label="wz60 <= wz5",fontsize=16,color="black",shape="box"];9826 -> 29256[label="",style="solid", color="black", weight=3];
9827[label="wz64",fontsize=16,color="green",shape="box"];9828[label="wz63",fontsize=16,color="green",shape="box"];9829[label="wz5",fontsize=16,color="green",shape="box"];9830[label="wz61",fontsize=16,color="green",shape="box"];9831[label="wz4",fontsize=16,color="green",shape="box"];9832[label="wz60",fontsize=16,color="green",shape="box"];9833[label="wz62",fontsize=16,color="green",shape="box"];9824[label="foldFM_LE1 wz498 wz499 wz500 wz501 wz502 wz503 wz504 wz505 wz506\n  Ord a",fontsize=16,color="burlywood",shape="triangle"];29637[label="wz506/False",fontsize=10,color="white",style="solid",shape="box"];9824 -> 29637[label="",style="solid", color="burlywood", weight=9];
29637 -> 29257[label="",style="solid", color="burlywood", weight=3];
29638[label="wz506/True",fontsize=10,color="white",style="solid",shape="box"];9824 -> 29638[label="",style="solid", color="burlywood", weight=9];
29638 -> 29258[label="",style="solid", color="burlywood", weight=3];
29256[label="compare wz60 wz5 /= GT",fontsize=16,color="black",shape="box"];29256 -> 29259[label="",style="solid", color="black", weight=3];
29257[label="foldFM_LE1 wz498 wz499 wz500 wz501 wz502 wz503 wz504 wz505 False\n  Ord a",fontsize=16,color="black",shape="box"];29257 -> 29260[label="",style="solid", color="black", weight=3];
29258[label="foldFM_LE1 wz498 wz499 wz500 wz501 wz502 wz503 wz504 wz505 True\n  Ord a",fontsize=16,color="black",shape="box"];29258 -> 29261[label="",style="solid", color="black", weight=3];
29259 -> 29446[label="",style="dashed", color="red", weight=0];
29259[label="not (compare wz60 wz5 == GT)",fontsize=16,color="magenta"];29259 -> 29447[label="",style="dashed", color="magenta", weight=3];
29260[label="foldFM_LE0 wz498 wz499 wz500 wz501 wz502 wz503 wz504 wz505 otherwise\n  Ord a",fontsize=16,color="black",shape="box"];29260 -> 29263[label="",style="solid", color="black", weight=3];
29261[label="foldFM_LE wz498 (wz498 wz501 wz502 (foldFM_LE wz498 wz499 wz500 wz504)) wz500 wz505\n  Ord a",fontsize=16,color="burlywood",shape="box"];29640[label="wz505/EmptyFM",fontsize=10,color="white",style="solid",shape="box"];29261 -> 29640[label="",style="solid", color="burlywood", weight=9];
29640 -> 29264[label="",style="solid", color="burlywood", weight=3];
29641[label="wz505/Branch wz5050 wz5051 wz5052 wz5053 wz5054",fontsize=10,color="white",style="solid",shape="box"];29261 -> 29641[label="",style="solid", color="burlywood", weight=9];
29641 -> 29265[label="",style="solid", color="burlywood", weight=3];
29447[label="compare wz60 wz5",fontsize=16,color="burlywood",shape="box"];29642[label="wz60/wz600 :% wz601",fontsize=10,color="white",style="solid",shape="box"];29447 -> 29642[label="",style="solid", color="burlywood", weight=9];
29642 -> 29479[label="",style="solid", color="burlywood", weight=3];
29446[label="not (wz511 == GT)",fontsize=16,color="burlywood",shape="triangle"];29643[label="wz511/LT",fontsize=10,color="white",style="solid",shape="box"];29446 -> 29643[label="",style="solid", color="burlywood", weight=9];
29643 -> 29480[label="",style="solid", color="burlywood", weight=3];
29644[label="wz511/EQ",fontsize=10,color="white",style="solid",shape="box"];29446 -> 29644[label="",style="solid", color="burlywood", weight=9];
29644 -> 29481[label="",style="solid", color="burlywood", weight=3];
29645[label="wz511/GT",fontsize=10,color="white",style="solid",shape="box"];29446 -> 29645[label="",style="solid", color="burlywood", weight=9];
29645 -> 29482[label="",style="solid", color="burlywood", weight=3];
29263[label="foldFM_LE0 wz498 wz499 wz500 wz501 wz502 wz503 wz504 wz505 True\n  Ord a",fontsize=16,color="black",shape="box"];29263 -> 29267[label="",style="solid", color="black", weight=3];
29264[label="foldFM_LE wz498 (wz498 wz501 wz502 (foldFM_LE wz498 wz499 wz500 wz504)) wz500 EmptyFM\n  Ord a",fontsize=16,color="black",shape="box"];29264 -> 29268[label="",style="solid", color="black", weight=3];
29265[label="foldFM_LE wz498 (wz498 wz501 wz502 (foldFM_LE wz498 wz499 wz500 wz504)) wz500 (Branch wz5050 wz5051 wz5052 wz5053 wz5054)\n  Ord a",fontsize=16,color="black",shape="box"];29265 -> 29269[label="",style="solid", color="black", weight=3];
29479[label="compare (wz600 :% wz601) wz5",fontsize=16,color="burlywood",shape="box"];29646[label="wz5/wz50 :% wz51",fontsize=10,color="white",style="solid",shape="box"];29479 -> 29646[label="",style="solid", color="burlywood", weight=9];
29646 -> 29497[label="",style="solid", color="burlywood", weight=3];
29480[label="not (LT == GT)",fontsize=16,color="black",shape="box"];29480 -> 29498[label="",style="solid", color="black", weight=3];
29481[label="not (EQ == GT)",fontsize=16,color="black",shape="box"];29481 -> 29499[label="",style="solid", color="black", weight=3];
29482[label="not (GT == GT)",fontsize=16,color="black",shape="box"];29482 -> 29500[label="",style="solid", color="black", weight=3];
29267[label="foldFM_LE wz498 wz499 wz500 wz504\n  Ord a",fontsize=16,color="burlywood",shape="triangle"];29647[label="wz504/EmptyFM",fontsize=10,color="white",style="solid",shape="box"];29267 -> 29647[label="",style="solid", color="burlywood", weight=9];
29647 -> 29271[label="",style="solid", color="burlywood", weight=3];
29648[label="wz504/Branch wz5040 wz5041 wz5042 wz5043 wz5044",fontsize=10,color="white",style="solid",shape="box"];29267 -> 29648[label="",style="solid", color="burlywood", weight=9];
29648 -> 29272[label="",style="solid", color="burlywood", weight=3];
29268 -> 29273[label="",style="dashed", color="red", weight=0];
29268[label="foldFM_LE3 wz498 (wz498 wz501 wz502 (foldFM_LE wz498 wz499 wz500 wz504)) wz500 EmptyFM\n  Ord a",fontsize=16,color="magenta"];29268 -> 29274[label="",style="dashed", color="magenta", weight=3];
29269 -> 29275[label="",style="dashed", color="red", weight=0];
29269[label="foldFM_LE2 wz498 (wz498 wz501 wz502 (foldFM_LE wz498 wz499 wz500 wz504)) wz500 (Branch wz5050 wz5051 wz5052 wz5053 wz5054)\n  Ord a",fontsize=16,color="magenta"];29269 -> 29276[label="",style="dashed", color="magenta", weight=3];
29497[label="compare (wz600 :% wz601) (wz50 :% wz51)",fontsize=16,color="black",shape="box"];29497 -> 29504[label="",style="solid", color="black", weight=3];
29498[label="not False",fontsize=16,color="black",shape="triangle"];29498 -> 29505[label="",style="solid", color="black", weight=3];
29499 -> 29498[label="",style="dashed", color="red", weight=0];
29499[label="not False",fontsize=16,color="magenta"];29500[label="not True",fontsize=16,color="black",shape="box"];29500 -> 29506[label="",style="solid", color="black", weight=3];
29271[label="foldFM_LE wz498 wz499 wz500 EmptyFM\n  Ord a",fontsize=16,color="black",shape="box"];29271 -> 29278[label="",style="solid", color="black", weight=3];
29272[label="foldFM_LE wz498 wz499 wz500 (Branch wz5040 wz5041 wz5042 wz5043 wz5044)\n  Ord a",fontsize=16,color="black",shape="box"];29272 -> 29279[label="",style="solid", color="black", weight=3];
29274 -> 29267[label="",style="dashed", color="red", weight=0];
29274[label="foldFM_LE wz498 wz499 wz500 wz504\n  Ord a",fontsize=16,color="magenta"];29273[label="foldFM_LE3 wz498 (wz498 wz501 wz502 wz507) wz500 EmptyFM\n  Ord a",fontsize=16,color="black",shape="triangle"];29273 -> 29280[label="",style="solid", color="black", weight=3];
29276 -> 29267[label="",style="dashed", color="red", weight=0];
29276[label="foldFM_LE wz498 wz499 wz500 wz504\n  Ord a",fontsize=16,color="magenta"];29275[label="foldFM_LE2 wz498 (wz498 wz501 wz502 wz508) wz500 (Branch wz5050 wz5051 wz5052 wz5053 wz5054)\n  Ord a",fontsize=16,color="black",shape="triangle"];29275 -> 29281[label="",style="solid", color="black", weight=3];
29504 -> 29465[label="",style="dashed", color="red", weight=0];
29504[label="compare (wz600 * wz51) (wz50 * wz601)",fontsize=16,color="magenta"];29504 -> 29512[label="",style="dashed", color="magenta", weight=3];
29504 -> 29513[label="",style="dashed", color="magenta", weight=3];
29505[label="True",fontsize=16,color="green",shape="box"];29506[label="False",fontsize=16,color="green",shape="box"];29278[label="foldFM_LE3 wz498 wz499 wz500 EmptyFM\n  Ord a",fontsize=16,color="black",shape="box"];29278 -> 29283[label="",style="solid", color="black", weight=3];
29279[label="foldFM_LE2 wz498 wz499 wz500 (Branch wz5040 wz5041 wz5042 wz5043 wz5044)\n  Ord a",fontsize=16,color="black",shape="box"];29279 -> 29284[label="",style="solid", color="black", weight=3];
29280[label="wz498 wz501 wz502 wz507\n  Ord a",fontsize=16,color="green",shape="box"];29280 -> 29285[label="",style="dashed", color="green", weight=3];
29280 -> 29286[label="",style="dashed", color="green", weight=3];
29280 -> 29287[label="",style="dashed", color="green", weight=3];
29281 -> 9824[label="",style="dashed", color="red", weight=0];
29281[label="foldFM_LE1 wz498 (wz498 wz501 wz502 wz508) wz500 wz5050 wz5051 wz5052 wz5053 wz5054 (wz5050 <= wz500)\n  Ord a",fontsize=16,color="magenta"];29281 -> 29288[label="",style="dashed", color="magenta", weight=3];
29281 -> 29289[label="",style="dashed", color="magenta", weight=3];
29281 -> 29290[label="",style="dashed", color="magenta", weight=3];
29281 -> 29291[label="",style="dashed", color="magenta", weight=3];
29281 -> 29292[label="",style="dashed", color="magenta", weight=3];
29281 -> 29293[label="",style="dashed", color="magenta", weight=3];
29281 -> 29294[label="",style="dashed", color="magenta", weight=3];
29512[label="wz600 * wz51",fontsize=16,color="black",shape="triangle"];29512 -> 29524[label="",style="solid", color="black", weight=3];
29513 -> 29512[label="",style="dashed", color="red", weight=0];
29513[label="wz50 * wz601",fontsize=16,color="magenta"];29513 -> 29525[label="",style="dashed", color="magenta", weight=3];
29513 -> 29526[label="",style="dashed", color="magenta", weight=3];
29465[label="compare wz5050 wz500",fontsize=16,color="black",shape="triangle"];29465 -> 29493[label="",style="solid", color="black", weight=3];
29283[label="wz499",fontsize=16,color="green",shape="box"];29284 -> 9824[label="",style="dashed", color="red", weight=0];
29284[label="foldFM_LE1 wz498 wz499 wz500 wz5040 wz5041 wz5042 wz5043 wz5044 (wz5040 <= wz500)\n  Ord a",fontsize=16,color="magenta"];29284 -> 29297[label="",style="dashed", color="magenta", weight=3];
29284 -> 29298[label="",style="dashed", color="magenta", weight=3];
29284 -> 29299[label="",style="dashed", color="magenta", weight=3];
29284 -> 29300[label="",style="dashed", color="magenta", weight=3];
29284 -> 29301[label="",style="dashed", color="magenta", weight=3];
29284 -> 29302[label="",style="dashed", color="magenta", weight=3];
29285[label="wz501\n  Ord a",fontsize=16,color="green",shape="box"];29286[label="wz502",fontsize=16,color="green",shape="box"];29287[label="wz507",fontsize=16,color="green",shape="box"];29288[label="wz5050 <= wz500\n  Ord a",fontsize=16,color="blue",shape="box"];29658[label="<= :: ([] a) -> ([] a) -> Bool",fontsize=10,color="white",style="solid",shape="box"];29288 -> 29658[label="",style="solid", color="blue", weight=9];
29658 -> 29303[label="",style="solid", color="blue", weight=3];
29659[label="<= :: Char -> Char -> Bool",fontsize=10,color="white",style="solid",shape="box"];29288 -> 29659[label="",style="solid", color="blue", weight=9];
29659 -> 29304[label="",style="solid", color="blue", weight=3];
29660[label="<= :: (Either a b) -> (Either a b) -> Bool",fontsize=10,color="white",style="solid",shape="box"];29288 -> 29660[label="",style="solid", color="blue", weight=9];
29660 -> 29305[label="",style="solid", color="blue", weight=3];
29661[label="<= :: Float -> Float -> Bool",fontsize=10,color="white",style="solid",shape="box"];29288 -> 29661[label="",style="solid", color="blue", weight=9];
29661 -> 29306[label="",style="solid", color="blue", weight=3];
29662[label="<= :: (Maybe a) -> (Maybe a) -> Bool",fontsize=10,color="white",style="solid",shape="box"];29288 -> 29662[label="",style="solid", color="blue", weight=9];
29662 -> 29307[label="",style="solid", color="blue", weight=3];
29663[label="<= :: Ordering -> Ordering -> Bool",fontsize=10,color="white",style="solid",shape="box"];29288 -> 29663[label="",style="solid", color="blue", weight=9];
29663 -> 29308[label="",style="solid", color="blue", weight=3];
29664[label="<= :: Double -> Double -> Bool",fontsize=10,color="white",style="solid",shape="box"];29288 -> 29664[label="",style="solid", color="blue", weight=9];
29664 -> 29309[label="",style="solid", color="blue", weight=3];
29665[label="<= :: (Ratio a) -> (Ratio a) -> Bool",fontsize=10,color="white",style="solid",shape="box"];29288 -> 29665[label="",style="solid", color="blue", weight=9];
29665 -> 29310[label="",style="solid", color="blue", weight=3];
29666[label="<= :: () -> () -> Bool",fontsize=10,color="white",style="solid",shape="box"];29288 -> 29666[label="",style="solid", color="blue", weight=9];
29666 -> 29311[label="",style="solid", color="blue", weight=3];
29667[label="<= :: ((@2) a b) -> ((@2) a b) -> Bool",fontsize=10,color="white",style="solid",shape="box"];29288 -> 29667[label="",style="solid", color="blue", weight=9];
29667 -> 29312[label="",style="solid", color="blue", weight=3];
29668[label="<= :: Int -> Int -> Bool",fontsize=10,color="white",style="solid",shape="box"];29288 -> 29668[label="",style="solid", color="blue", weight=9];
29668 -> 29313[label="",style="solid", color="blue", weight=3];
29669[label="<= :: Integer -> Integer -> Bool",fontsize=10,color="white",style="solid",shape="box"];29288 -> 29669[label="",style="solid", color="blue", weight=9];
29669 -> 29314[label="",style="solid", color="blue", weight=3];
29670[label="<= :: Bool -> Bool -> Bool",fontsize=10,color="white",style="solid",shape="box"];29288 -> 29670[label="",style="solid", color="blue", weight=9];
29670 -> 29315[label="",style="solid", color="blue", weight=3];
29671[label="<= :: ((@3) a b c) -> ((@3) a b c) -> Bool",fontsize=10,color="white",style="solid",shape="box"];29288 -> 29671[label="",style="solid", color="blue", weight=9];
29671 -> 29316[label="",style="solid", color="blue", weight=3];
29289[label="wz5054\n  Ord a",fontsize=16,color="green",shape="box"];29290[label="wz5053\n  Ord a",fontsize=16,color="green",shape="box"];29291[label="wz5051",fontsize=16,color="green",shape="box"];29292[label="wz498 wz501 wz502 wz508\n  Ord a",fontsize=16,color="green",shape="box"];29292 -> 29317[label="",style="dashed", color="green", weight=3];
29292 -> 29318[label="",style="dashed", color="green", weight=3];
29292 -> 29319[label="",style="dashed", color="green", weight=3];
29293[label="wz5050\n  Ord a",fontsize=16,color="green",shape="box"];29294[label="wz5052",fontsize=16,color="green",shape="box"];29524[label="primMulInt wz600 wz51",fontsize=16,color="burlywood",shape="box"];29672[label="wz600/Pos wz6000",fontsize=10,color="white",style="solid",shape="box"];29524 -> 29672[label="",style="solid", color="burlywood", weight=9];
29672 -> 29543[label="",style="solid", color="burlywood", weight=3];
29673[label="wz600/Neg wz6000",fontsize=10,color="white",style="solid",shape="box"];29524 -> 29673[label="",style="solid", color="burlywood", weight=9];
29673 -> 29544[label="",style="solid", color="burlywood", weight=3];
29525[label="wz601",fontsize=16,color="green",shape="box"];29526[label="wz50",fontsize=16,color="green",shape="box"];29493[label="primCmpInt wz5050 wz500",fontsize=16,color="burlywood",shape="box"];29674[label="wz5050/Pos wz50500",fontsize=10,color="white",style="solid",shape="box"];29493 -> 29674[label="",style="solid", color="burlywood", weight=9];
29674 -> 29502[label="",style="solid", color="burlywood", weight=3];
29675[label="wz5050/Neg wz50500",fontsize=10,color="white",style="solid",shape="box"];29493 -> 29675[label="",style="solid", color="burlywood", weight=9];
29675 -> 29503[label="",style="solid", color="burlywood", weight=3];
29297[label="wz5040 <= wz500\n  Ord a",fontsize=16,color="blue",shape="box"];29676[label="<= :: ([] a) -> ([] a) -> Bool",fontsize=10,color="white",style="solid",shape="box"];29297 -> 29676[label="",style="solid", color="blue", weight=9];
29676 -> 29324[label="",style="solid", color="blue", weight=3];
29677[label="<= :: Char -> Char -> Bool",fontsize=10,color="white",style="solid",shape="box"];29297 -> 29677[label="",style="solid", color="blue", weight=9];
29677 -> 29325[label="",style="solid", color="blue", weight=3];
29678[label="<= :: (Either a b) -> (Either a b) -> Bool",fontsize=10,color="white",style="solid",shape="box"];29297 -> 29678[label="",style="solid", color="blue", weight=9];
29678 -> 29326[label="",style="solid", color="blue", weight=3];
29679[label="<= :: Float -> Float -> Bool",fontsize=10,color="white",style="solid",shape="box"];29297 -> 29679[label="",style="solid", color="blue", weight=9];
29679 -> 29327[label="",style="solid", color="blue", weight=3];
29680[label="<= :: (Maybe a) -> (Maybe a) -> Bool",fontsize=10,color="white",style="solid",shape="box"];29297 -> 29680[label="",style="solid", color="blue", weight=9];
29680 -> 29328[label="",style="solid", color="blue", weight=3];
29681[label="<= :: Ordering -> Ordering -> Bool",fontsize=10,color="white",style="solid",shape="box"];29297 -> 29681[label="",style="solid", color="blue", weight=9];
29681 -> 29329[label="",style="solid", color="blue", weight=3];
29682[label="<= :: Double -> Double -> Bool",fontsize=10,color="white",style="solid",shape="box"];29297 -> 29682[label="",style="solid", color="blue", weight=9];
29682 -> 29330[label="",style="solid", color="blue", weight=3];
29683[label="<= :: (Ratio a) -> (Ratio a) -> Bool",fontsize=10,color="white",style="solid",shape="box"];29297 -> 29683[label="",style="solid", color="blue", weight=9];
29683 -> 29331[label="",style="solid", color="blue", weight=3];
29684[label="<= :: () -> () -> Bool",fontsize=10,color="white",style="solid",shape="box"];29297 -> 29684[label="",style="solid", color="blue", weight=9];
29684 -> 29332[label="",style="solid", color="blue", weight=3];
29685[label="<= :: ((@2) a b) -> ((@2) a b) -> Bool",fontsize=10,color="white",style="solid",shape="box"];29297 -> 29685[label="",style="solid", color="blue", weight=9];
29685 -> 29333[label="",style="solid", color="blue", weight=3];
29686[label="<= :: Int -> Int -> Bool",fontsize=10,color="white",style="solid",shape="box"];29297 -> 29686[label="",style="solid", color="blue", weight=9];
29686 -> 29334[label="",style="solid", color="blue", weight=3];
29687[label="<= :: Integer -> Integer -> Bool",fontsize=10,color="white",style="solid",shape="box"];29297 -> 29687[label="",style="solid", color="blue", weight=9];
29687 -> 29335[label="",style="solid", color="blue", weight=3];
29688[label="<= :: Bool -> Bool -> Bool",fontsize=10,color="white",style="solid",shape="box"];29297 -> 29688[label="",style="solid", color="blue", weight=9];
29688 -> 29336[label="",style="solid", color="blue", weight=3];
29689[label="<= :: ((@3) a b c) -> ((@3) a b c) -> Bool",fontsize=10,color="white",style="solid",shape="box"];29297 -> 29689[label="",style="solid", color="blue", weight=9];
29689 -> 29337[label="",style="solid", color="blue", weight=3];
29298[label="wz5044\n  Ord a",fontsize=16,color="green",shape="box"];29299[label="wz5043\n  Ord a",fontsize=16,color="green",shape="box"];29300[label="wz5041",fontsize=16,color="green",shape="box"];29301[label="wz5040\n  Ord a",fontsize=16,color="green",shape="box"];29302[label="wz5042",fontsize=16,color="green",shape="box"];29303[label="wz5050 <= wz500\n  Ord a",fontsize=16,color="black",shape="triangle"];29303 -> 29338[label="",style="solid", color="black", weight=3];
29304[label="wz5050 <= wz500",fontsize=16,color="black",shape="triangle"];29304 -> 29339[label="",style="solid", color="black", weight=3];
29305[label="wz5050 <= wz500\n  Ord a  Ord b",fontsize=16,color="black",shape="triangle"];29305 -> 29340[label="",style="solid", color="black", weight=3];
29306[label="wz5050 <= wz500",fontsize=16,color="black",shape="triangle"];29306 -> 29341[label="",style="solid", color="black", weight=3];
29307[label="wz5050 <= wz500\n  Ord a",fontsize=16,color="black",shape="triangle"];29307 -> 29342[label="",style="solid", color="black", weight=3];
29308[label="wz5050 <= wz500",fontsize=16,color="black",shape="triangle"];29308 -> 29343[label="",style="solid", color="black", weight=3];
29309[label="wz5050 <= wz500",fontsize=16,color="black",shape="triangle"];29309 -> 29344[label="",style="solid", color="black", weight=3];
29310[label="wz5050 <= wz500\n  Integral a",fontsize=16,color="black",shape="triangle"];29310 -> 29345[label="",style="solid", color="black", weight=3];
29311[label="wz5050 <= wz500",fontsize=16,color="black",shape="triangle"];29311 -> 29346[label="",style="solid", color="black", weight=3];
29312[label="wz5050 <= wz500\n  Ord a  Ord b",fontsize=16,color="black",shape="triangle"];29312 -> 29347[label="",style="solid", color="black", weight=3];
29313[label="wz5050 <= wz500",fontsize=16,color="black",shape="triangle"];29313 -> 29348[label="",style="solid", color="black", weight=3];
29314[label="wz5050 <= wz500",fontsize=16,color="black",shape="triangle"];29314 -> 29349[label="",style="solid", color="black", weight=3];
29315[label="wz5050 <= wz500",fontsize=16,color="black",shape="triangle"];29315 -> 29350[label="",style="solid", color="black", weight=3];
29316[label="wz5050 <= wz500\n  Ord a  Ord b  Ord c",fontsize=16,color="black",shape="triangle"];29316 -> 29351[label="",style="solid", color="black", weight=3];
29317[label="wz501\n  Ord a",fontsize=16,color="green",shape="box"];29318[label="wz502",fontsize=16,color="green",shape="box"];29319[label="wz508",fontsize=16,color="green",shape="box"];29543[label="primMulInt (Pos wz6000) wz51",fontsize=16,color="burlywood",shape="box"];29690[label="wz51/Pos wz510",fontsize=10,color="white",style="solid",shape="box"];29543 -> 29690[label="",style="solid", color="burlywood", weight=9];
29690 -> 29564[label="",style="solid", color="burlywood", weight=3];
29691[label="wz51/Neg wz510",fontsize=10,color="white",style="solid",shape="box"];29543 -> 29691[label="",style="solid", color="burlywood", weight=9];
29691 -> 29565[label="",style="solid", color="burlywood", weight=3];
29544[label="primMulInt (Neg wz6000) wz51",fontsize=16,color="burlywood",shape="box"];29692[label="wz51/Pos wz510",fontsize=10,color="white",style="solid",shape="box"];29544 -> 29692[label="",style="solid", color="burlywood", weight=9];
29692 -> 29566[label="",style="solid", color="burlywood", weight=3];
29693[label="wz51/Neg wz510",fontsize=10,color="white",style="solid",shape="box"];29544 -> 29693[label="",style="solid", color="burlywood", weight=9];
29693 -> 29567[label="",style="solid", color="burlywood", weight=3];
29502[label="primCmpInt (Pos wz50500) wz500",fontsize=16,color="burlywood",shape="box"];29694[label="wz50500/Succ wz505000",fontsize=10,color="white",style="solid",shape="box"];29502 -> 29694[label="",style="solid", color="burlywood", weight=9];
29694 -> 29508[label="",style="solid", color="burlywood", weight=3];
29695[label="wz50500/Zero",fontsize=10,color="white",style="solid",shape="box"];29502 -> 29695[label="",style="solid", color="burlywood", weight=9];
29695 -> 29509[label="",style="solid", color="burlywood", weight=3];
29503[label="primCmpInt (Neg wz50500) wz500",fontsize=16,color="burlywood",shape="box"];29696[label="wz50500/Succ wz505000",fontsize=10,color="white",style="solid",shape="box"];29503 -> 29696[label="",style="solid", color="burlywood", weight=9];
29696 -> 29510[label="",style="solid", color="burlywood", weight=3];
29697[label="wz50500/Zero",fontsize=10,color="white",style="solid",shape="box"];29503 -> 29697[label="",style="solid", color="burlywood", weight=9];
29697 -> 29511[label="",style="solid", color="burlywood", weight=3];
29324 -> 29303[label="",style="dashed", color="red", weight=0];
29324[label="wz5040 <= wz500\n  Ord a",fontsize=16,color="magenta"];29324 -> 29356[label="",style="dashed", color="magenta", weight=3];
29325 -> 29304[label="",style="dashed", color="red", weight=0];
29325[label="wz5040 <= wz500",fontsize=16,color="magenta"];29325 -> 29357[label="",style="dashed", color="magenta", weight=3];
29326 -> 29305[label="",style="dashed", color="red", weight=0];
29326[label="wz5040 <= wz500\n  Ord a  Ord b",fontsize=16,color="magenta"];29326 -> 29358[label="",style="dashed", color="magenta", weight=3];
29327 -> 29306[label="",style="dashed", color="red", weight=0];
29327[label="wz5040 <= wz500",fontsize=16,color="magenta"];29327 -> 29359[label="",style="dashed", color="magenta", weight=3];
29328 -> 29307[label="",style="dashed", color="red", weight=0];
29328[label="wz5040 <= wz500\n  Ord a",fontsize=16,color="magenta"];29328 -> 29360[label="",style="dashed", color="magenta", weight=3];
29329 -> 29308[label="",style="dashed", color="red", weight=0];
29329[label="wz5040 <= wz500",fontsize=16,color="magenta"];29329 -> 29361[label="",style="dashed", color="magenta", weight=3];
29330 -> 29309[label="",style="dashed", color="red", weight=0];
29330[label="wz5040 <= wz500",fontsize=16,color="magenta"];29330 -> 29362[label="",style="dashed", color="magenta", weight=3];
29331 -> 29310[label="",style="dashed", color="red", weight=0];
29331[label="wz5040 <= wz500\n  Integral a",fontsize=16,color="magenta"];29331 -> 29363[label="",style="dashed", color="magenta", weight=3];
29332 -> 29311[label="",style="dashed", color="red", weight=0];
29332[label="wz5040 <= wz500",fontsize=16,color="magenta"];29332 -> 29364[label="",style="dashed", color="magenta", weight=3];
29333 -> 29312[label="",style="dashed", color="red", weight=0];
29333[label="wz5040 <= wz500\n  Ord a  Ord b",fontsize=16,color="magenta"];29333 -> 29365[label="",style="dashed", color="magenta", weight=3];
29334 -> 29313[label="",style="dashed", color="red", weight=0];
29334[label="wz5040 <= wz500",fontsize=16,color="magenta"];29334 -> 29366[label="",style="dashed", color="magenta", weight=3];
29335 -> 29314[label="",style="dashed", color="red", weight=0];
29335[label="wz5040 <= wz500",fontsize=16,color="magenta"];29335 -> 29367[label="",style="dashed", color="magenta", weight=3];
29336 -> 29315[label="",style="dashed", color="red", weight=0];
29336[label="wz5040 <= wz500",fontsize=16,color="magenta"];29336 -> 29368[label="",style="dashed", color="magenta", weight=3];
29337 -> 29316[label="",style="dashed", color="red", weight=0];
29337[label="wz5040 <= wz500\n  Ord a  Ord b  Ord c",fontsize=16,color="magenta"];29337 -> 29369[label="",style="dashed", color="magenta", weight=3];
29338[label="compare wz5050 wz500 /= GT\n  Ord a",fontsize=16,color="black",shape="box"];29338 -> 29370[label="",style="solid", color="black", weight=3];
29339[label="compare wz5050 wz500 /= GT",fontsize=16,color="black",shape="box"];29339 -> 29371[label="",style="solid", color="black", weight=3];
29340[label="compare wz5050 wz500 /= GT\n  Ord a  Ord b",fontsize=16,color="black",shape="box"];29340 -> 29372[label="",style="solid", color="black", weight=3];
29341[label="compare wz5050 wz500 /= GT",fontsize=16,color="black",shape="box"];29341 -> 29373[label="",style="solid", color="black", weight=3];
29342[label="compare wz5050 wz500 /= GT\n  Ord a",fontsize=16,color="black",shape="box"];29342 -> 29374[label="",style="solid", color="black", weight=3];
29343[label="compare wz5050 wz500 /= GT",fontsize=16,color="black",shape="box"];29343 -> 29375[label="",style="solid", color="black", weight=3];
29344[label="compare wz5050 wz500 /= GT",fontsize=16,color="black",shape="box"];29344 -> 29376[label="",style="solid", color="black", weight=3];
29345[label="compare wz5050 wz500 /= GT\n  Integral a",fontsize=16,color="black",shape="box"];29345 -> 29377[label="",style="solid", color="black", weight=3];
29346[label="compare wz5050 wz500 /= GT",fontsize=16,color="black",shape="box"];29346 -> 29378[label="",style="solid", color="black", weight=3];
29347[label="compare wz5050 wz500 /= GT\n  Ord a  Ord b",fontsize=16,color="black",shape="box"];29347 -> 29379[label="",style="solid", color="black", weight=3];
29348[label="compare wz5050 wz500 /= GT",fontsize=16,color="black",shape="box"];29348 -> 29380[label="",style="solid", color="black", weight=3];
29349[label="compare wz5050 wz500 /= GT",fontsize=16,color="black",shape="box"];29349 -> 29381[label="",style="solid", color="black", weight=3];
29350[label="compare wz5050 wz500 /= GT",fontsize=16,color="black",shape="box"];29350 -> 29382[label="",style="solid", color="black", weight=3];
29351[label="compare wz5050 wz500 /= GT\n  Ord a  Ord b  Ord c",fontsize=16,color="black",shape="box"];29351 -> 29383[label="",style="solid", color="black", weight=3];
29564[label="primMulInt (Pos wz6000) (Pos wz510)",fontsize=16,color="black",shape="box"];29564 -> 29576[label="",style="solid", color="black", weight=3];
29565[label="primMulInt (Pos wz6000) (Neg wz510)",fontsize=16,color="black",shape="box"];29565 -> 29577[label="",style="solid", color="black", weight=3];
29566[label="primMulInt (Neg wz6000) (Pos wz510)",fontsize=16,color="black",shape="box"];29566 -> 29578[label="",style="solid", color="black", weight=3];
29567[label="primMulInt (Neg wz6000) (Neg wz510)",fontsize=16,color="black",shape="box"];29567 -> 29579[label="",style="solid", color="black", weight=3];
29508[label="primCmpInt (Pos (Succ wz505000)) wz500",fontsize=16,color="burlywood",shape="box"];29712[label="wz500/Pos wz5000",fontsize=10,color="white",style="solid",shape="box"];29508 -> 29712[label="",style="solid", color="burlywood", weight=9];
29712 -> 29516[label="",style="solid", color="burlywood", weight=3];
29713[label="wz500/Neg wz5000",fontsize=10,color="white",style="solid",shape="box"];29508 -> 29713[label="",style="solid", color="burlywood", weight=9];
29713 -> 29517[label="",style="solid", color="burlywood", weight=3];
29509[label="primCmpInt (Pos Zero) wz500",fontsize=16,color="burlywood",shape="box"];29714[label="wz500/Pos wz5000",fontsize=10,color="white",style="solid",shape="box"];29509 -> 29714[label="",style="solid", color="burlywood", weight=9];
29714 -> 29518[label="",style="solid", color="burlywood", weight=3];
29715[label="wz500/Neg wz5000",fontsize=10,color="white",style="solid",shape="box"];29509 -> 29715[label="",style="solid", color="burlywood", weight=9];
29715 -> 29519[label="",style="solid", color="burlywood", weight=3];
29510[label="primCmpInt (Neg (Succ wz505000)) wz500",fontsize=16,color="burlywood",shape="box"];29716[label="wz500/Pos wz5000",fontsize=10,color="white",style="solid",shape="box"];29510 -> 29716[label="",style="solid", color="burlywood", weight=9];
29716 -> 29520[label="",style="solid", color="burlywood", weight=3];
29717[label="wz500/Neg wz5000",fontsize=10,color="white",style="solid",shape="box"];29510 -> 29717[label="",style="solid", color="burlywood", weight=9];
29717 -> 29521[label="",style="solid", color="burlywood", weight=3];
29511[label="primCmpInt (Neg Zero) wz500",fontsize=16,color="burlywood",shape="box"];29718[label="wz500/Pos wz5000",fontsize=10,color="white",style="solid",shape="box"];29511 -> 29718[label="",style="solid", color="burlywood", weight=9];
29718 -> 29522[label="",style="solid", color="burlywood", weight=3];
29719[label="wz500/Neg wz5000",fontsize=10,color="white",style="solid",shape="box"];29511 -> 29719[label="",style="solid", color="burlywood", weight=9];
29719 -> 29523[label="",style="solid", color="burlywood", weight=3];
29356[label="wz5040\n  Ord a",fontsize=16,color="green",shape="box"];29357[label="wz5040",fontsize=16,color="green",shape="box"];29358[label="wz5040\n  Ord a  Ord b",fontsize=16,color="green",shape="box"];29359[label="wz5040",fontsize=16,color="green",shape="box"];29360[label="wz5040\n  Ord a",fontsize=16,color="green",shape="box"];29361[label="wz5040",fontsize=16,color="green",shape="box"];29362[label="wz5040",fontsize=16,color="green",shape="box"];29363[label="wz5040\n  Integral a",fontsize=16,color="green",shape="box"];29364[label="wz5040",fontsize=16,color="green",shape="box"];29365[label="wz5040\n  Ord a  Ord b",fontsize=16,color="green",shape="box"];29366[label="wz5040",fontsize=16,color="green",shape="box"];29367[label="wz5040",fontsize=16,color="green",shape="box"];29368[label="wz5040",fontsize=16,color="green",shape="box"];29369[label="wz5040\n  Ord a  Ord b  Ord c",fontsize=16,color="green",shape="box"];29370 -> 29446[label="",style="dashed", color="red", weight=0];
29370[label="not (compare wz5050 wz500 == GT)\n  Ord a",fontsize=16,color="magenta"];29370 -> 29455[label="",style="dashed", color="magenta", weight=3];
29371 -> 29446[label="",style="dashed", color="red", weight=0];
29371[label="not (compare wz5050 wz500 == GT)",fontsize=16,color="magenta"];29371 -> 29456[label="",style="dashed", color="magenta", weight=3];
29372 -> 29446[label="",style="dashed", color="red", weight=0];
29372[label="not (compare wz5050 wz500 == GT)\n  Ord a  Ord b",fontsize=16,color="magenta"];29372 -> 29457[label="",style="dashed", color="magenta", weight=3];
29373 -> 29446[label="",style="dashed", color="red", weight=0];
29373[label="not (compare wz5050 wz500 == GT)",fontsize=16,color="magenta"];29373 -> 29458[label="",style="dashed", color="magenta", weight=3];
29374 -> 29446[label="",style="dashed", color="red", weight=0];
29374[label="not (compare wz5050 wz500 == GT)\n  Ord a",fontsize=16,color="magenta"];29374 -> 29459[label="",style="dashed", color="magenta", weight=3];
29375 -> 29446[label="",style="dashed", color="red", weight=0];
29375[label="not (compare wz5050 wz500 == GT)",fontsize=16,color="magenta"];29375 -> 29460[label="",style="dashed", color="magenta", weight=3];
29376 -> 29446[label="",style="dashed", color="red", weight=0];
29376[label="not (compare wz5050 wz500 == GT)",fontsize=16,color="magenta"];29376 -> 29461[label="",style="dashed", color="magenta", weight=3];
29377 -> 29446[label="",style="dashed", color="red", weight=0];
29377[label="not (compare wz5050 wz500 == GT)\n  Integral a",fontsize=16,color="magenta"];29377 -> 29462[label="",style="dashed", color="magenta", weight=3];
29378 -> 29446[label="",style="dashed", color="red", weight=0];
29378[label="not (compare wz5050 wz500 == GT)",fontsize=16,color="magenta"];29378 -> 29463[label="",style="dashed", color="magenta", weight=3];
29379 -> 29446[label="",style="dashed", color="red", weight=0];
29379[label="not (compare wz5050 wz500 == GT)\n  Ord a  Ord b",fontsize=16,color="magenta"];29379 -> 29464[label="",style="dashed", color="magenta", weight=3];
29380 -> 29446[label="",style="dashed", color="red", weight=0];
29380[label="not (compare wz5050 wz500 == GT)",fontsize=16,color="magenta"];29380 -> 29465[label="",style="dashed", color="magenta", weight=3];
29381 -> 29446[label="",style="dashed", color="red", weight=0];
29381[label="not (compare wz5050 wz500 == GT)",fontsize=16,color="magenta"];29381 -> 29466[label="",style="dashed", color="magenta", weight=3];
29382 -> 29446[label="",style="dashed", color="red", weight=0];
29382[label="not (compare wz5050 wz500 == GT)",fontsize=16,color="magenta"];29382 -> 29467[label="",style="dashed", color="magenta", weight=3];
29383 -> 29446[label="",style="dashed", color="red", weight=0];
29383[label="not (compare wz5050 wz500 == GT)\n  Ord a  Ord b  Ord c",fontsize=16,color="magenta"];29383 -> 29468[label="",style="dashed", color="magenta", weight=3];
29576[label="Pos (primMulNat wz6000 wz510)",fontsize=16,color="green",shape="box"];29576 -> 29584[label="",style="dashed", color="green", weight=3];
29577[label="Neg (primMulNat wz6000 wz510)",fontsize=16,color="green",shape="box"];29577 -> 29585[label="",style="dashed", color="green", weight=3];
29578[label="Neg (primMulNat wz6000 wz510)",fontsize=16,color="green",shape="box"];29578 -> 29586[label="",style="dashed", color="green", weight=3];
29579[label="Pos (primMulNat wz6000 wz510)",fontsize=16,color="green",shape="box"];29579 -> 29587[label="",style="dashed", color="green", weight=3];
29516[label="primCmpInt (Pos (Succ wz505000)) (Pos wz5000)",fontsize=16,color="black",shape="box"];29516 -> 29531[label="",style="solid", color="black", weight=3];
29517[label="primCmpInt (Pos (Succ wz505000)) (Neg wz5000)",fontsize=16,color="black",shape="box"];29517 -> 29532[label="",style="solid", color="black", weight=3];
29518[label="primCmpInt (Pos Zero) (Pos wz5000)",fontsize=16,color="burlywood",shape="box"];29734[label="wz5000/Succ wz50000",fontsize=10,color="white",style="solid",shape="box"];29518 -> 29734[label="",style="solid", color="burlywood", weight=9];
29734 -> 29533[label="",style="solid", color="burlywood", weight=3];
29735[label="wz5000/Zero",fontsize=10,color="white",style="solid",shape="box"];29518 -> 29735[label="",style="solid", color="burlywood", weight=9];
29735 -> 29534[label="",style="solid", color="burlywood", weight=3];
29519[label="primCmpInt (Pos Zero) (Neg wz5000)",fontsize=16,color="burlywood",shape="box"];29736[label="wz5000/Succ wz50000",fontsize=10,color="white",style="solid",shape="box"];29519 -> 29736[label="",style="solid", color="burlywood", weight=9];
29736 -> 29535[label="",style="solid", color="burlywood", weight=3];
29737[label="wz5000/Zero",fontsize=10,color="white",style="solid",shape="box"];29519 -> 29737[label="",style="solid", color="burlywood", weight=9];
29737 -> 29536[label="",style="solid", color="burlywood", weight=3];
29520[label="primCmpInt (Neg (Succ wz505000)) (Pos wz5000)",fontsize=16,color="black",shape="box"];29520 -> 29537[label="",style="solid", color="black", weight=3];
29521[label="primCmpInt (Neg (Succ wz505000)) (Neg wz5000)",fontsize=16,color="black",shape="box"];29521 -> 29538[label="",style="solid", color="black", weight=3];
29522[label="primCmpInt (Neg Zero) (Pos wz5000)",fontsize=16,color="burlywood",shape="box"];29738[label="wz5000/Succ wz50000",fontsize=10,color="white",style="solid",shape="box"];29522 -> 29738[label="",style="solid", color="burlywood", weight=9];
29738 -> 29539[label="",style="solid", color="burlywood", weight=3];
29739[label="wz5000/Zero",fontsize=10,color="white",style="solid",shape="box"];29522 -> 29739[label="",style="solid", color="burlywood", weight=9];
29739 -> 29540[label="",style="solid", color="burlywood", weight=3];
29523[label="primCmpInt (Neg Zero) (Neg wz5000)",fontsize=16,color="burlywood",shape="box"];29740[label="wz5000/Succ wz50000",fontsize=10,color="white",style="solid",shape="box"];29523 -> 29740[label="",style="solid", color="burlywood", weight=9];
29740 -> 29541[label="",style="solid", color="burlywood", weight=3];
29741[label="wz5000/Zero",fontsize=10,color="white",style="solid",shape="box"];29523 -> 29741[label="",style="solid", color="burlywood", weight=9];
29741 -> 29542[label="",style="solid", color="burlywood", weight=3];
29455[label="compare wz5050 wz500\n  Ord a",fontsize=16,color="black",shape="box"];29455 -> 29483[label="",style="solid", color="black", weight=3];
29456[label="compare wz5050 wz500",fontsize=16,color="black",shape="box"];29456 -> 29484[label="",style="solid", color="black", weight=3];
29457[label="compare wz5050 wz500\n  Ord a  Ord b",fontsize=16,color="black",shape="box"];29457 -> 29485[label="",style="solid", color="black", weight=3];
29458[label="compare wz5050 wz500",fontsize=16,color="black",shape="box"];29458 -> 29486[label="",style="solid", color="black", weight=3];
29459[label="compare wz5050 wz500\n  Ord a",fontsize=16,color="black",shape="box"];29459 -> 29487[label="",style="solid", color="black", weight=3];
29460[label="compare wz5050 wz500",fontsize=16,color="black",shape="box"];29460 -> 29488[label="",style="solid", color="black", weight=3];
29461[label="compare wz5050 wz500",fontsize=16,color="black",shape="box"];29461 -> 29489[label="",style="solid", color="black", weight=3];
29462[label="compare wz5050 wz500\n  Integral a",fontsize=16,color="burlywood",shape="box"];29742[label="wz5050/wz50500 :% wz50501",fontsize=10,color="white",style="solid",shape="box"];29462 -> 29742[label="",style="solid", color="burlywood", weight=9];
29742 -> 29490[label="",style="solid", color="burlywood", weight=3];
29463[label="compare wz5050 wz500",fontsize=16,color="black",shape="box"];29463 -> 29491[label="",style="solid", color="black", weight=3];
29464[label="compare wz5050 wz500\n  Ord a  Ord b",fontsize=16,color="black",shape="box"];29464 -> 29492[label="",style="solid", color="black", weight=3];
29466[label="compare wz5050 wz500",fontsize=16,color="black",shape="triangle"];29466 -> 29494[label="",style="solid", color="black", weight=3];
29467[label="compare wz5050 wz500",fontsize=16,color="black",shape="box"];29467 -> 29495[label="",style="solid", color="black", weight=3];
29468[label="compare wz5050 wz500\n  Ord a  Ord b  Ord c",fontsize=16,color="black",shape="box"];29468 -> 29496[label="",style="solid", color="black", weight=3];
29584[label="primMulNat wz6000 wz510",fontsize=16,color="burlywood",shape="triangle"];29743[label="wz6000/Succ wz60000",fontsize=10,color="white",style="solid",shape="box"];29584 -> 29743[label="",style="solid", color="burlywood", weight=9];
29743 -> 29592[label="",style="solid", color="burlywood", weight=3];
29744[label="wz6000/Zero",fontsize=10,color="white",style="solid",shape="box"];29584 -> 29744[label="",style="solid", color="burlywood", weight=9];
29744 -> 29593[label="",style="solid", color="burlywood", weight=3];
29585 -> 29584[label="",style="dashed", color="red", weight=0];
29585[label="primMulNat wz6000 wz510",fontsize=16,color="magenta"];29585 -> 29594[label="",style="dashed", color="magenta", weight=3];
29586 -> 29584[label="",style="dashed", color="red", weight=0];
29586[label="primMulNat wz6000 wz510",fontsize=16,color="magenta"];29586 -> 29595[label="",style="dashed", color="magenta", weight=3];
29587 -> 29584[label="",style="dashed", color="red", weight=0];
29587[label="primMulNat wz6000 wz510",fontsize=16,color="magenta"];29587 -> 29596[label="",style="dashed", color="magenta", weight=3];
29587 -> 29597[label="",style="dashed", color="magenta", weight=3];
29531[label="primCmpNat (Succ wz505000) wz5000",fontsize=16,color="burlywood",shape="triangle"];29748[label="wz5000/Succ wz50000",fontsize=10,color="white",style="solid",shape="box"];29531 -> 29748[label="",style="solid", color="burlywood", weight=9];
29748 -> 29552[label="",style="solid", color="burlywood", weight=3];
29749[label="wz5000/Zero",fontsize=10,color="white",style="solid",shape="box"];29531 -> 29749[label="",style="solid", color="burlywood", weight=9];
29749 -> 29553[label="",style="solid", color="burlywood", weight=3];
29532[label="GT",fontsize=16,color="green",shape="box"];29533[label="primCmpInt (Pos Zero) (Pos (Succ wz50000))",fontsize=16,color="black",shape="box"];29533 -> 29554[label="",style="solid", color="black", weight=3];
29534[label="primCmpInt (Pos Zero) (Pos Zero)",fontsize=16,color="black",shape="box"];29534 -> 29555[label="",style="solid", color="black", weight=3];
29535[label="primCmpInt (Pos Zero) (Neg (Succ wz50000))",fontsize=16,color="black",shape="box"];29535 -> 29556[label="",style="solid", color="black", weight=3];
29536[label="primCmpInt (Pos Zero) (Neg Zero)",fontsize=16,color="black",shape="box"];29536 -> 29557[label="",style="solid", color="black", weight=3];
29537[label="LT",fontsize=16,color="green",shape="box"];29538[label="primCmpNat wz5000 (Succ wz505000)",fontsize=16,color="burlywood",shape="triangle"];29750[label="wz5000/Succ wz50000",fontsize=10,color="white",style="solid",shape="box"];29538 -> 29750[label="",style="solid", color="burlywood", weight=9];
29750 -> 29558[label="",style="solid", color="burlywood", weight=3];
29751[label="wz5000/Zero",fontsize=10,color="white",style="solid",shape="box"];29538 -> 29751[label="",style="solid", color="burlywood", weight=9];
29751 -> 29559[label="",style="solid", color="burlywood", weight=3];
29539[label="primCmpInt (Neg Zero) (Pos (Succ wz50000))",fontsize=16,color="black",shape="box"];29539 -> 29560[label="",style="solid", color="black", weight=3];
29540[label="primCmpInt (Neg Zero) (Pos Zero)",fontsize=16,color="black",shape="box"];29540 -> 29561[label="",style="solid", color="black", weight=3];
29541[label="primCmpInt (Neg Zero) (Neg (Succ wz50000))",fontsize=16,color="black",shape="box"];29541 -> 29562[label="",style="solid", color="black", weight=3];
29542[label="primCmpInt (Neg Zero) (Neg Zero)",fontsize=16,color="black",shape="box"];29542 -> 29563[label="",style="solid", color="black", weight=3];
29483[label="error []",fontsize=16,color="red",shape="box"];29484[label="error []",fontsize=16,color="red",shape="box"];29485[label="error []",fontsize=16,color="red",shape="box"];29486[label="error []",fontsize=16,color="red",shape="box"];29487[label="error []",fontsize=16,color="red",shape="box"];29488[label="error []",fontsize=16,color="red",shape="box"];29489[label="error []",fontsize=16,color="red",shape="box"];29490[label="compare (wz50500 :% wz50501) wz500\n  Integral a",fontsize=16,color="burlywood",shape="box"];29752[label="wz500/wz5000 :% wz5001",fontsize=10,color="white",style="solid",shape="box"];29490 -> 29752[label="",style="solid", color="burlywood", weight=9];
29752 -> 29501[label="",style="solid", color="burlywood", weight=3];
29491[label="error []",fontsize=16,color="red",shape="box"];29492[label="error []",fontsize=16,color="red",shape="box"];29494[label="error []",fontsize=16,color="red",shape="box"];29495[label="error []",fontsize=16,color="red",shape="box"];29496[label="error []",fontsize=16,color="red",shape="box"];29592[label="primMulNat (Succ wz60000) wz510",fontsize=16,color="burlywood",shape="box"];29753[label="wz510/Succ wz5100",fontsize=10,color="white",style="solid",shape="box"];29592 -> 29753[label="",style="solid", color="burlywood", weight=9];
29753 -> 29602[label="",style="solid", color="burlywood", weight=3];
29754[label="wz510/Zero",fontsize=10,color="white",style="solid",shape="box"];29592 -> 29754[label="",style="solid", color="burlywood", weight=9];
29754 -> 29603[label="",style="solid", color="burlywood", weight=3];
29593[label="primMulNat Zero wz510",fontsize=16,color="burlywood",shape="box"];29755[label="wz510/Succ wz5100",fontsize=10,color="white",style="solid",shape="box"];29593 -> 29755[label="",style="solid", color="burlywood", weight=9];
29755 -> 29604[label="",style="solid", color="burlywood", weight=3];
29756[label="wz510/Zero",fontsize=10,color="white",style="solid",shape="box"];29593 -> 29756[label="",style="solid", color="burlywood", weight=9];
29756 -> 29605[label="",style="solid", color="burlywood", weight=3];
29594[label="wz510",fontsize=16,color="green",shape="box"];29595[label="wz6000",fontsize=16,color="green",shape="box"];29596[label="wz510",fontsize=16,color="green",shape="box"];29597[label="wz6000",fontsize=16,color="green",shape="box"];29552[label="primCmpNat (Succ wz505000) (Succ wz50000)",fontsize=16,color="black",shape="box"];29552 -> 29568[label="",style="solid", color="black", weight=3];
29553[label="primCmpNat (Succ wz505000) Zero",fontsize=16,color="black",shape="box"];29553 -> 29569[label="",style="solid", color="black", weight=3];
29554 -> 29538[label="",style="dashed", color="red", weight=0];
29554[label="primCmpNat Zero (Succ wz50000)",fontsize=16,color="magenta"];29554 -> 29570[label="",style="dashed", color="magenta", weight=3];
29554 -> 29571[label="",style="dashed", color="magenta", weight=3];
29555[label="EQ",fontsize=16,color="green",shape="box"];29556[label="GT",fontsize=16,color="green",shape="box"];29557[label="EQ",fontsize=16,color="green",shape="box"];29558[label="primCmpNat (Succ wz50000) (Succ wz505000)",fontsize=16,color="black",shape="box"];29558 -> 29572[label="",style="solid", color="black", weight=3];
29559[label="primCmpNat Zero (Succ wz505000)",fontsize=16,color="black",shape="box"];29559 -> 29573[label="",style="solid", color="black", weight=3];
29560[label="LT",fontsize=16,color="green",shape="box"];29561[label="EQ",fontsize=16,color="green",shape="box"];29562 -> 29531[label="",style="dashed", color="red", weight=0];
29562[label="primCmpNat (Succ wz50000) Zero",fontsize=16,color="magenta"];29562 -> 29574[label="",style="dashed", color="magenta", weight=3];
29562 -> 29575[label="",style="dashed", color="magenta", weight=3];
29563[label="EQ",fontsize=16,color="green",shape="box"];29501[label="compare (wz50500 :% wz50501) (wz5000 :% wz5001)\n  Integral a",fontsize=16,color="black",shape="box"];29501 -> 29507[label="",style="solid", color="black", weight=3];
29602[label="primMulNat (Succ wz60000) (Succ wz5100)",fontsize=16,color="black",shape="box"];29602 -> 29608[label="",style="solid", color="black", weight=3];
29603[label="primMulNat (Succ wz60000) Zero",fontsize=16,color="black",shape="box"];29603 -> 29609[label="",style="solid", color="black", weight=3];
29604[label="primMulNat Zero (Succ wz5100)",fontsize=16,color="black",shape="box"];29604 -> 29610[label="",style="solid", color="black", weight=3];
29605[label="primMulNat Zero Zero",fontsize=16,color="black",shape="box"];29605 -> 29611[label="",style="solid", color="black", weight=3];
29568[label="primCmpNat wz505000 wz50000",fontsize=16,color="burlywood",shape="triangle"];29759[label="wz505000/Succ wz5050000",fontsize=10,color="white",style="solid",shape="box"];29568 -> 29759[label="",style="solid", color="burlywood", weight=9];
29759 -> 29580[label="",style="solid", color="burlywood", weight=3];
29760[label="wz505000/Zero",fontsize=10,color="white",style="solid",shape="box"];29568 -> 29760[label="",style="solid", color="burlywood", weight=9];
29760 -> 29581[label="",style="solid", color="burlywood", weight=3];
29569[label="GT",fontsize=16,color="green",shape="box"];29570[label="Zero",fontsize=16,color="green",shape="box"];29571[label="wz50000",fontsize=16,color="green",shape="box"];29572 -> 29568[label="",style="dashed", color="red", weight=0];
29572[label="primCmpNat wz50000 wz505000",fontsize=16,color="magenta"];29572 -> 29582[label="",style="dashed", color="magenta", weight=3];
29572 -> 29583[label="",style="dashed", color="magenta", weight=3];
29573[label="LT",fontsize=16,color="green",shape="box"];29574[label="Zero",fontsize=16,color="green",shape="box"];29575[label="wz50000",fontsize=16,color="green",shape="box"];29507[label="compare (wz50500 * wz5001) (wz5000 * wz50501)\n  Integral a",fontsize=16,color="blue",shape="box"];29762[label="compare :: Int -> Int -> Ordering",fontsize=10,color="white",style="solid",shape="box"];29507 -> 29762[label="",style="solid", color="blue", weight=9];
29762 -> 29514[label="",style="solid", color="blue", weight=3];
29763[label="compare :: Integer -> Integer -> Ordering",fontsize=10,color="white",style="solid",shape="box"];29507 -> 29763[label="",style="solid", color="blue", weight=9];
29763 -> 29515[label="",style="solid", color="blue", weight=3];
29608 -> 29612[label="",style="dashed", color="red", weight=0];
29608[label="primPlusNat (primMulNat wz60000 (Succ wz5100)) (Succ wz5100)",fontsize=16,color="magenta"];29608 -> 29613[label="",style="dashed", color="magenta", weight=3];
29609[label="Zero",fontsize=16,color="green",shape="box"];29610[label="Zero",fontsize=16,color="green",shape="box"];29611[label="Zero",fontsize=16,color="green",shape="box"];29580[label="primCmpNat (Succ wz5050000) wz50000",fontsize=16,color="burlywood",shape="box"];29765[label="wz50000/Succ wz500000",fontsize=10,color="white",style="solid",shape="box"];29580 -> 29765[label="",style="solid", color="burlywood", weight=9];
29765 -> 29588[label="",style="solid", color="burlywood", weight=3];
29766[label="wz50000/Zero",fontsize=10,color="white",style="solid",shape="box"];29580 -> 29766[label="",style="solid", color="burlywood", weight=9];
29766 -> 29589[label="",style="solid", color="burlywood", weight=3];
29581[label="primCmpNat Zero wz50000",fontsize=16,color="burlywood",shape="box"];29767[label="wz50000/Succ wz500000",fontsize=10,color="white",style="solid",shape="box"];29581 -> 29767[label="",style="solid", color="burlywood", weight=9];
29767 -> 29590[label="",style="solid", color="burlywood", weight=3];
29768[label="wz50000/Zero",fontsize=10,color="white",style="solid",shape="box"];29581 -> 29768[label="",style="solid", color="burlywood", weight=9];
29768 -> 29591[label="",style="solid", color="burlywood", weight=3];
29582[label="wz505000",fontsize=16,color="green",shape="box"];29583[label="wz50000",fontsize=16,color="green",shape="box"];29514 -> 29465[label="",style="dashed", color="red", weight=0];
29514[label="compare (wz50500 * wz5001) (wz5000 * wz50501)",fontsize=16,color="magenta"];29514 -> 29527[label="",style="dashed", color="magenta", weight=3];
29514 -> 29528[label="",style="dashed", color="magenta", weight=3];
29515 -> 29466[label="",style="dashed", color="red", weight=0];
29515[label="compare (wz50500 * wz5001) (wz5000 * wz50501)",fontsize=16,color="magenta"];29515 -> 29529[label="",style="dashed", color="magenta", weight=3];
29515 -> 29530[label="",style="dashed", color="magenta", weight=3];
29613 -> 29584[label="",style="dashed", color="red", weight=0];
29613[label="primMulNat wz60000 (Succ wz5100)",fontsize=16,color="magenta"];29613 -> 29614[label="",style="dashed", color="magenta", weight=3];
29613 -> 29615[label="",style="dashed", color="magenta", weight=3];
29612[label="primPlusNat wz512 (Succ wz5100)",fontsize=16,color="burlywood",shape="triangle"];29772[label="wz512/Succ wz5120",fontsize=10,color="white",style="solid",shape="box"];29612 -> 29772[label="",style="solid", color="burlywood", weight=9];
29772 -> 29616[label="",style="solid", color="burlywood", weight=3];
29773[label="wz512/Zero",fontsize=10,color="white",style="solid",shape="box"];29612 -> 29773[label="",style="solid", color="burlywood", weight=9];
29773 -> 29617[label="",style="solid", color="burlywood", weight=3];
29588[label="primCmpNat (Succ wz5050000) (Succ wz500000)",fontsize=16,color="black",shape="box"];29588 -> 29598[label="",style="solid", color="black", weight=3];
29589[label="primCmpNat (Succ wz5050000) Zero",fontsize=16,color="black",shape="box"];29589 -> 29599[label="",style="solid", color="black", weight=3];
29590[label="primCmpNat Zero (Succ wz500000)",fontsize=16,color="black",shape="box"];29590 -> 29600[label="",style="solid", color="black", weight=3];
29591[label="primCmpNat Zero Zero",fontsize=16,color="black",shape="box"];29591 -> 29601[label="",style="solid", color="black", weight=3];
29527 -> 29512[label="",style="dashed", color="red", weight=0];
29527[label="wz50500 * wz5001",fontsize=16,color="magenta"];29527 -> 29545[label="",style="dashed", color="magenta", weight=3];
29527 -> 29546[label="",style="dashed", color="magenta", weight=3];
29528 -> 29512[label="",style="dashed", color="red", weight=0];
29528[label="wz5000 * wz50501",fontsize=16,color="magenta"];29528 -> 29547[label="",style="dashed", color="magenta", weight=3];
29528 -> 29548[label="",style="dashed", color="magenta", weight=3];
29529[label="wz50500 * wz5001",fontsize=16,color="black",shape="triangle"];29529 -> 29549[label="",style="solid", color="black", weight=3];
29530 -> 29529[label="",style="dashed", color="red", weight=0];
29530[label="wz5000 * wz50501",fontsize=16,color="magenta"];29530 -> 29550[label="",style="dashed", color="magenta", weight=3];
29530 -> 29551[label="",style="dashed", color="magenta", weight=3];
29614[label="Succ wz5100",fontsize=16,color="green",shape="box"];29615[label="wz60000",fontsize=16,color="green",shape="box"];29616[label="primPlusNat (Succ wz5120) (Succ wz5100)",fontsize=16,color="black",shape="box"];29616 -> 29618[label="",style="solid", color="black", weight=3];
29617[label="primPlusNat Zero (Succ wz5100)",fontsize=16,color="black",shape="box"];29617 -> 29619[label="",style="solid", color="black", weight=3];
29598 -> 29568[label="",style="dashed", color="red", weight=0];
29598[label="primCmpNat wz5050000 wz500000",fontsize=16,color="magenta"];29598 -> 29606[label="",style="dashed", color="magenta", weight=3];
29598 -> 29607[label="",style="dashed", color="magenta", weight=3];
29599[label="GT",fontsize=16,color="green",shape="box"];29600[label="LT",fontsize=16,color="green",shape="box"];29601[label="EQ",fontsize=16,color="green",shape="box"];29545[label="wz5001",fontsize=16,color="green",shape="box"];29546[label="wz50500",fontsize=16,color="green",shape="box"];29547[label="wz50501",fontsize=16,color="green",shape="box"];29548[label="wz5000",fontsize=16,color="green",shape="box"];29549[label="error []",fontsize=16,color="red",shape="box"];29550[label="wz5000",fontsize=16,color="green",shape="box"];29551[label="wz50501",fontsize=16,color="green",shape="box"];29618[label="Succ (Succ (primPlusNat wz5120 wz5100))",fontsize=16,color="green",shape="box"];29618 -> 29620[label="",style="dashed", color="green", weight=3];
29619[label="Succ wz5100",fontsize=16,color="green",shape="box"];29606[label="wz500000",fontsize=16,color="green",shape="box"];29607[label="wz5050000",fontsize=16,color="green",shape="box"];29620[label="primPlusNat wz5120 wz5100",fontsize=16,color="burlywood",shape="triangle"];29778[label="wz5120/Succ wz51200",fontsize=10,color="white",style="solid",shape="box"];29620 -> 29778[label="",style="solid", color="burlywood", weight=9];
29778 -> 29621[label="",style="solid", color="burlywood", weight=3];
29779[label="wz5120/Zero",fontsize=10,color="white",style="solid",shape="box"];29620 -> 29779[label="",style="solid", color="burlywood", weight=9];
29779 -> 29622[label="",style="solid", color="burlywood", weight=3];
29621[label="primPlusNat (Succ wz51200) wz5100",fontsize=16,color="burlywood",shape="box"];29780[label="wz5100/Succ wz51000",fontsize=10,color="white",style="solid",shape="box"];29621 -> 29780[label="",style="solid", color="burlywood", weight=9];
29780 -> 29623[label="",style="solid", color="burlywood", weight=3];
29781[label="wz5100/Zero",fontsize=10,color="white",style="solid",shape="box"];29621 -> 29781[label="",style="solid", color="burlywood", weight=9];
29781 -> 29624[label="",style="solid", color="burlywood", weight=3];
29622[label="primPlusNat Zero wz5100",fontsize=16,color="burlywood",shape="box"];29782[label="wz5100/Succ wz51000",fontsize=10,color="white",style="solid",shape="box"];29622 -> 29782[label="",style="solid", color="burlywood", weight=9];
29782 -> 29625[label="",style="solid", color="burlywood", weight=3];
29783[label="wz5100/Zero",fontsize=10,color="white",style="solid",shape="box"];29622 -> 29783[label="",style="solid", color="burlywood", weight=9];
29783 -> 29626[label="",style="solid", color="burlywood", weight=3];
29623[label="primPlusNat (Succ wz51200) (Succ wz51000)",fontsize=16,color="black",shape="box"];29623 -> 29627[label="",style="solid", color="black", weight=3];
29624[label="primPlusNat (Succ wz51200) Zero",fontsize=16,color="black",shape="box"];29624 -> 29628[label="",style="solid", color="black", weight=3];
29625[label="primPlusNat Zero (Succ wz51000)",fontsize=16,color="black",shape="box"];29625 -> 29629[label="",style="solid", color="black", weight=3];
29626[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="box"];29626 -> 29630[label="",style="solid", color="black", weight=3];
29627[label="Succ (Succ (primPlusNat wz51200 wz51000))",fontsize=16,color="green",shape="box"];29627 -> 29631[label="",style="dashed", color="green", weight=3];
29628[label="Succ wz51200",fontsize=16,color="green",shape="box"];29629[label="Succ wz51000",fontsize=16,color="green",shape="box"];29630[label="Zero",fontsize=16,color="green",shape="box"];29631 -> 29620[label="",style="dashed", color="red", weight=0];
29631[label="primPlusNat wz51200 wz51000",fontsize=16,color="magenta"];29631 -> 29632[label="",style="dashed", color="magenta", weight=3];
29631 -> 29633[label="",style="dashed", color="magenta", weight=3];
29632[label="wz51000",fontsize=16,color="green",shape="box"];29633[label="wz51200",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ Narrow

            ↳ AND

              ↳ QDP

                ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(wz51200), Succ(wz51000)) → new_primPlusNat(wz51200, wz51000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_primPlusNat(Succ(wz51200), Succ(wz51000)) → new_primPlusNat(wz51200, wz51000)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ Narrow

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(wz60000), Succ(wz5100)) → new_primMulNat(wz60000, Succ(wz5100))

From the DPs we obtained the following set of size-change graphs:

new_primMulNat(Succ(wz60000), Succ(wz5100)) → new_primMulNat(wz60000, Succ(wz5100))
The graph contains the following edges 1 > 1, 2 >= 2

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ Narrow

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPSizeChangeProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primCmpNat(Succ(wz5050000), Succ(wz500000)) → new_primCmpNat(wz5050000, wz500000)

From the DPs we obtained the following set of size-change graphs:

new_primCmpNat(Succ(wz5050000), Succ(wz500000)) → new_primCmpNat(wz5050000, wz500000)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ Narrow

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

new_foldFM_LE(wz498, wz500, Branch(wz5040, wz5041, wz5042, wz5043, wz5044), h, ba, bb) → new_foldFM_LE1(wz498, wz500, wz5040, wz5041, wz5042, wz5043, wz5044, new_ltEs(wz5040, wz500, ba), h, ba, bb)
new_foldFM_LE1(wz498, wz500, wz501, wz502, wz503, wz504, Branch(wz5050, wz5051, wz5052, wz5053, wz5054), True, h, ba, bb) → new_foldFM_LE(wz498, wz500, wz504, h, ba, bb)
new_foldFM_LE1(wz498, wz500, wz501, wz502, wz503, Branch(wz5040, wz5041, wz5042, wz5043, wz5044), wz505, False, h, ba, bb) → new_foldFM_LE1(wz498, wz500, wz5040, wz5041, wz5042, wz5043, wz5044, new_ltEs(wz5040, wz500, ba), h, ba, bb)
new_foldFM_LE1(wz498, wz500, wz501, wz502, wz503, wz504, Branch(wz5050, wz5051, wz5052, wz5053, wz5054), True, h, ba, bb) → new_foldFM_LE2(wz498, wz501, wz502, wz500, wz5050, wz5051, wz5052, wz5053, wz5054, h, ba, bb)
new_foldFM_LE2(wz498, wz501, wz502, wz500, wz5050, wz5051, wz5052, wz5053, wz5054, h, ba, bb) → new_foldFM_LE1(wz498, wz500, wz5050, wz5051, wz5052, wz5053, wz5054, new_ltEs0(wz5050, wz500, ba), h, ba, bb)
new_foldFM_LE1(wz498, wz500, wz501, wz502, wz503, wz504, EmptyFM, True, h, ba, bb) → new_foldFM_LE(wz498, wz500, wz504, h, ba, bb)

The TRS R consists of the following rules:

new_ltEs(wz5040, wz500, app(ty_[], bc)) → new_ltEs4(wz5040, wz500, bc)
new_sr(Neg(wz6000), Neg(wz510)) → Pos(new_primMulNat0(wz6000, wz510))
new_ltEs9(wz5050, wz500, bg) → new_not(new_compare1(wz5050, wz500, bg))
new_compare(Neg(Zero), Neg(Zero)) → EQ
new_ltEs0(wz5050, wz500, ty_Integer) → new_ltEs12(wz5050, wz500)
new_primCmpNat1(Succ(wz5050000), Succ(wz500000)) → new_primCmpNat1(wz5050000, wz500000)
new_compare0(wz5050, wz500) → error([])
new_ltEs(wz5040, wz500, ty_Ordering) → new_ltEs7(wz5040, wz500)
new_ltEs0(wz5050, wz500, ty_Double) → new_ltEs8(wz5050, wz500)
new_foldFM_LE0(wz498, wz499, wz500, Branch(wz5040, wz5041, wz5042, wz5043, wz5044), h, ba, bb) → new_foldFM_LE10(wz498, wz499, wz500, wz5040, wz5041, wz5042, wz5043, wz5044, new_ltEs(wz5040, wz500, ba), h, ba, bb)
new_compare1(:%(wz50500, wz50501), :%(wz5000, wz5001), ty_Integer) → new_compare0(new_sr0(wz50500, wz5001), new_sr0(wz5000, wz50501))
new_primCmpNat2(Zero, wz505000) → LT
new_sr(Pos(wz6000), Pos(wz510)) → Pos(new_primMulNat0(wz6000, wz510))
new_ltEs(wz5040, wz500, ty_@0) → new_ltEs10(wz5040, wz500)
new_ltEs2(wz5050, wz500) → new_not(error([]))
new_compare(Pos(Zero), Neg(Zero)) → EQ
new_compare(Neg(Zero), Pos(Zero)) → EQ
new_ltEs5(wz5050, wz500, bd, be) → new_not(error([]))
new_sr0(wz50500, wz5001) → error([])
new_ltEs8(wz5050, wz500) → new_not(error([]))
new_ltEs0(wz5050, wz500, app(ty_Ratio, bg)) → new_ltEs9(wz5050, wz500, bg)
new_primPlusNat1(Zero, wz5100) → Succ(wz5100)
new_ltEs0(wz5050, wz500, app(app(app(ty_@3, cb), cc), cd)) → new_ltEs14(wz5050, wz500, cb, cc, cd)
new_primMulNat0(Succ(wz60000), Zero) → Zero
new_primMulNat0(Zero, Succ(wz5100)) → Zero
new_ltEs0(wz5050, wz500, ty_Char) → new_ltEs2(wz5050, wz500)
new_ltEs(wz5040, wz500, ty_Double) → new_ltEs8(wz5040, wz500)
new_ltEs(wz5040, wz500, ty_Float) → new_ltEs3(wz5040, wz500)
new_ltEs(wz5040, wz500, app(app(ty_Either, bd), be)) → new_ltEs5(wz5040, wz500, bd, be)
new_ltEs0(wz5050, wz500, ty_Float) → new_ltEs3(wz5050, wz500)
new_primMulNat0(Succ(wz60000), Succ(wz5100)) → new_primPlusNat1(new_primMulNat0(wz60000, Succ(wz5100)), wz5100)
new_primPlusNat0(Succ(wz51200), Succ(wz51000)) → Succ(Succ(new_primPlusNat0(wz51200, wz51000)))
new_foldFM_LE0(wz498, wz499, wz500, EmptyFM, h, ba, bb) → wz499
new_compare(Neg(Succ(wz505000)), Neg(wz5000)) → new_primCmpNat2(wz5000, wz505000)
new_compare(Pos(Zero), Pos(Succ(wz50000))) → new_primCmpNat2(Zero, wz50000)
new_ltEs0(wz5050, wz500, ty_Int) → new_ltEs1(wz5050, wz500)
new_primCmpNat1(Zero, Succ(wz500000)) → LT
new_primPlusNat0(Zero, Zero) → Zero
new_ltEs11(wz5050, wz500, bh, ca) → new_not(error([]))
new_primCmpNat2(Succ(wz50000), wz505000) → new_primCmpNat1(wz50000, wz505000)
new_ltEs0(wz5050, wz500, app(app(ty_Either, bd), be)) → new_ltEs5(wz5050, wz500, bd, be)
new_not(EQ) → new_not0
new_ltEs0(wz5050, wz500, app(app(ty_@2, bh), ca)) → new_ltEs11(wz5050, wz500, bh, ca)
new_ltEs(wz5040, wz500, ty_Bool) → new_ltEs13(wz5040, wz500)
new_ltEs6(wz5050, wz500, bf) → new_not(error([]))
new_ltEs(wz5040, wz500, app(app(ty_@2, bh), ca)) → new_ltEs11(wz5040, wz500, bh, ca)
new_primCmpNat1(Zero, Zero) → EQ
new_primCmpNat0(wz505000, Zero) → GT
new_ltEs(wz5040, wz500, ty_Int) → new_ltEs1(wz5040, wz500)
new_ltEs1(wz5050, wz500) → new_not(new_compare(wz5050, wz500))
new_primMulNat0(Zero, Zero) → Zero
new_ltEs(wz5040, wz500, app(ty_Maybe, bf)) → new_ltEs6(wz5040, wz500, bf)
new_compare(Neg(Zero), Pos(Succ(wz50000))) → LT
new_primPlusNat1(Succ(wz5120), wz5100) → Succ(Succ(new_primPlusNat0(wz5120, wz5100)))
new_ltEs7(wz5050, wz500) → new_not(error([]))
new_ltEs10(wz5050, wz500) → new_not(error([]))
new_ltEs0(wz5050, wz500, ty_@0) → new_ltEs10(wz5050, wz500)
new_ltEs(wz5040, wz500, ty_Char) → new_ltEs2(wz5040, wz500)
new_ltEs4(wz5050, wz500, bc) → new_not(error([]))
new_ltEs(wz5040, wz500, ty_Integer) → new_ltEs12(wz5040, wz500)
new_ltEs(wz5040, wz500, app(ty_Ratio, bg)) → new_ltEs9(wz5040, wz500, bg)
new_ltEs12(wz5050, wz500) → new_not(new_compare0(wz5050, wz500))
new_primCmpNat1(Succ(wz5050000), Zero) → GT
new_compare(Pos(Succ(wz505000)), Neg(wz5000)) → GT
new_compare(Pos(Succ(wz505000)), Pos(wz5000)) → new_primCmpNat0(wz505000, wz5000)
new_ltEs0(wz5050, wz500, app(ty_[], bc)) → new_ltEs4(wz5050, wz500, bc)
new_ltEs(wz5040, wz500, app(app(app(ty_@3, cb), cc), cd)) → new_ltEs14(wz5040, wz500, cb, cc, cd)
new_not(GT) → False
new_compare(Pos(Zero), Neg(Succ(wz50000))) → GT
new_compare1(:%(wz50500, wz50501), :%(wz5000, wz5001), ty_Int) → new_compare(new_sr(wz50500, wz5001), new_sr(wz5000, wz50501))
new_not0 → True
new_compare(Neg(Succ(wz505000)), Pos(wz5000)) → LT
new_sr(Pos(wz6000), Neg(wz510)) → Neg(new_primMulNat0(wz6000, wz510))
new_sr(Neg(wz6000), Pos(wz510)) → Neg(new_primMulNat0(wz6000, wz510))
new_compare(Neg(Zero), Neg(Succ(wz50000))) → new_primCmpNat0(wz50000, Zero)
new_ltEs0(wz5050, wz500, ty_Ordering) → new_ltEs7(wz5050, wz500)
new_compare(Pos(Zero), Pos(Zero)) → EQ
new_ltEs3(wz5050, wz500) → new_not(error([]))
new_ltEs0(wz5050, wz500, ty_Bool) → new_ltEs13(wz5050, wz500)
new_ltEs13(wz5050, wz500) → new_not(error([]))
new_primCmpNat0(wz505000, Succ(wz50000)) → new_primCmpNat1(wz505000, wz50000)
new_ltEs0(wz5050, wz500, app(ty_Maybe, bf)) → new_ltEs6(wz5050, wz500, bf)
new_primPlusNat0(Zero, Succ(wz51000)) → Succ(wz51000)
new_primPlusNat0(Succ(wz51200), Zero) → Succ(wz51200)
new_not(LT) → new_not0
new_ltEs14(wz5050, wz500, cb, cc, cd) → new_not(error([]))

The set Q consists of the following terms:

new_ltEs0(x0, x1, ty_Char)
new_not(GT)
new_compare1(:%(x0, x1), :%(x2, x3), ty_Integer)
new_ltEs0(x0, x1, ty_@0)
new_ltEs0(x0, x1, ty_Double)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Zero, Succ(x0))
new_compare0(x0, x1)
new_primMulNat0(Zero, Zero)
new_primPlusNat1(Zero, x0)
new_ltEs(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs(x0, x1, app(ty_Ratio, x2))
new_sr(Pos(x0), Pos(x1))
new_ltEs0(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs(x0, x1, app(app(ty_@2, x2), x3))
new_foldFM_LE0(x0, x1, x2, Branch(x3, x4, x5, x6, x7), x8, x9, x10)
new_primCmpNat0(x0, Zero)
new_ltEs10(x0, x1)
new_primPlusNat0(Succ(x0), Succ(x1))
new_ltEs0(x0, x1, ty_Integer)
new_ltEs(x0, x1, ty_Int)
new_primCmpNat0(x0, Succ(x1))
new_ltEs7(x0, x1)
new_ltEs8(x0, x1)
new_ltEs0(x0, x1, ty_Bool)
new_ltEs0(x0, x1, app(ty_Maybe, x2))
new_ltEs(x0, x1, ty_Ordering)
new_compare(Neg(Succ(x0)), Neg(x1))
new_ltEs0(x0, x1, app(app(ty_@2, x2), x3))
new_compare(Neg(Zero), Neg(Succ(x0)))
new_compare(Pos(Zero), Neg(Zero))
new_compare(Neg(Zero), Pos(Zero))
new_ltEs4(x0, x1, x2)
new_ltEs11(x0, x1, x2, x3)
new_not0
new_primPlusNat0(Zero, Zero)
new_compare(Pos(Succ(x0)), Pos(x1))
new_ltEs(x0, x1, ty_@0)
new_ltEs(x0, x1, ty_Bool)
new_ltEs0(x0, x1, ty_Ordering)
new_sr0(x0, x1)
new_primCmpNat2(Succ(x0), x1)
new_primPlusNat0(Succ(x0), Zero)
new_primCmpNat1(Succ(x0), Zero)
new_primCmpNat1(Zero, Zero)
new_ltEs3(x0, x1)
new_not(EQ)
new_ltEs(x0, x1, ty_Float)
new_compare(Neg(Zero), Neg(Zero))
new_ltEs0(x0, x1, app(ty_Ratio, x2))
new_compare(Pos(Zero), Pos(Zero))
new_primPlusNat1(Succ(x0), x1)
new_primCmpNat1(Zero, Succ(x0))
new_ltEs0(x0, x1, app(ty_[], x2))
new_ltEs1(x0, x1)
new_ltEs(x0, x1, ty_Double)
new_ltEs(x0, x1, app(ty_Maybe, x2))
new_ltEs13(x0, x1)
new_ltEs(x0, x1, ty_Integer)
new_sr(Neg(x0), Neg(x1))
new_foldFM_LE0(x0, x1, x2, EmptyFM, x3, x4, x5)
new_compare1(:%(x0, x1), :%(x2, x3), ty_Int)
new_ltEs0(x0, x1, ty_Int)
new_ltEs(x0, x1, ty_Char)
new_ltEs0(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs12(x0, x1)
new_primMulNat0(Succ(x0), Succ(x1))
new_ltEs6(x0, x1, x2)
new_compare(Pos(Zero), Pos(Succ(x0)))
new_not(LT)
new_primCmpNat2(Zero, x0)
new_ltEs(x0, x1, app(ty_[], x2))
new_primPlusNat0(Zero, Succ(x0))
new_primCmpNat1(Succ(x0), Succ(x1))
new_ltEs14(x0, x1, x2, x3, x4)
new_ltEs5(x0, x1, x2, x3)
new_compare(Neg(Succ(x0)), Pos(x1))
new_compare(Pos(Succ(x0)), Neg(x1))
new_ltEs2(x0, x1)
new_compare(Pos(Zero), Neg(Succ(x0)))
new_compare(Neg(Zero), Pos(Succ(x0)))
new_ltEs9(x0, x1, x2)
new_ltEs0(x0, x1, ty_Float)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ Narrow

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

new_foldFM_LE(wz498, wz500, Branch(wz5040, wz5041, wz5042, wz5043, wz5044), h, ba, bb) → new_foldFM_LE1(wz498, wz500, wz5040, wz5041, wz5042, wz5043, wz5044, new_ltEs(wz5040, wz500, ba), h, ba, bb)
new_foldFM_LE1(wz498, wz500, wz501, wz502, wz503, wz504, Branch(wz5050, wz5051, wz5052, wz5053, wz5054), True, h, ba, bb) → new_foldFM_LE(wz498, wz500, wz504, h, ba, bb)
new_foldFM_LE1(wz498, wz500, wz501, wz502, wz503, Branch(wz5040, wz5041, wz5042, wz5043, wz5044), wz505, False, h, ba, bb) → new_foldFM_LE1(wz498, wz500, wz5040, wz5041, wz5042, wz5043, wz5044, new_ltEs(wz5040, wz500, ba), h, ba, bb)
new_foldFM_LE1(wz498, wz500, wz501, wz502, wz503, wz504, Branch(wz5050, wz5051, wz5052, wz5053, wz5054), True, h, ba, bb) → new_foldFM_LE2(wz498, wz501, wz502, wz500, wz5050, wz5051, wz5052, wz5053, wz5054, h, ba, bb)
new_foldFM_LE2(wz498, wz501, wz502, wz500, wz5050, wz5051, wz5052, wz5053, wz5054, h, ba, bb) → new_foldFM_LE1(wz498, wz500, wz5050, wz5051, wz5052, wz5053, wz5054, new_ltEs0(wz5050, wz500, ba), h, ba, bb)
new_foldFM_LE1(wz498, wz500, wz501, wz502, wz503, wz504, EmptyFM, True, h, ba, bb) → new_foldFM_LE(wz498, wz500, wz504, h, ba, bb)

The TRS R consists of the following rules:

new_ltEs0(wz5050, wz500, ty_Integer) → new_ltEs12(wz5050, wz500)
new_ltEs0(wz5050, wz500, ty_Double) → new_ltEs8(wz5050, wz500)
new_ltEs0(wz5050, wz500, app(ty_Ratio, bg)) → new_ltEs9(wz5050, wz500, bg)
new_ltEs0(wz5050, wz500, app(app(app(ty_@3, cb), cc), cd)) → new_ltEs14(wz5050, wz500, cb, cc, cd)
new_ltEs0(wz5050, wz500, ty_Char) → new_ltEs2(wz5050, wz500)
new_ltEs0(wz5050, wz500, ty_Float) → new_ltEs3(wz5050, wz500)
new_ltEs0(wz5050, wz500, ty_Int) → new_ltEs1(wz5050, wz500)
new_ltEs0(wz5050, wz500, app(app(ty_Either, bd), be)) → new_ltEs5(wz5050, wz500, bd, be)
new_ltEs0(wz5050, wz500, app(app(ty_@2, bh), ca)) → new_ltEs11(wz5050, wz500, bh, ca)
new_ltEs0(wz5050, wz500, ty_@0) → new_ltEs10(wz5050, wz500)
new_ltEs0(wz5050, wz500, app(ty_[], bc)) → new_ltEs4(wz5050, wz500, bc)
new_ltEs0(wz5050, wz500, ty_Ordering) → new_ltEs7(wz5050, wz500)
new_ltEs0(wz5050, wz500, ty_Bool) → new_ltEs13(wz5050, wz500)
new_ltEs0(wz5050, wz500, app(ty_Maybe, bf)) → new_ltEs6(wz5050, wz500, bf)
new_ltEs6(wz5050, wz500, bf) → new_not(error([]))
new_ltEs13(wz5050, wz500) → new_not(error([]))
new_ltEs7(wz5050, wz500) → new_not(error([]))
new_ltEs4(wz5050, wz500, bc) → new_not(error([]))
new_ltEs10(wz5050, wz500) → new_not(error([]))
new_ltEs11(wz5050, wz500, bh, ca) → new_not(error([]))
new_ltEs5(wz5050, wz500, bd, be) → new_not(error([]))
new_ltEs1(wz5050, wz500) → new_not(new_compare(wz5050, wz500))
new_compare(Neg(Zero), Neg(Zero)) → EQ
new_compare(Pos(Zero), Neg(Zero)) → EQ
new_compare(Neg(Zero), Pos(Zero)) → EQ
new_compare(Neg(Succ(wz505000)), Neg(wz5000)) → new_primCmpNat2(wz5000, wz505000)
new_compare(Pos(Zero), Pos(Succ(wz50000))) → new_primCmpNat2(Zero, wz50000)
new_compare(Neg(Zero), Pos(Succ(wz50000))) → LT
new_compare(Pos(Succ(wz505000)), Neg(wz5000)) → GT
new_compare(Pos(Succ(wz505000)), Pos(wz5000)) → new_primCmpNat0(wz505000, wz5000)
new_compare(Pos(Zero), Neg(Succ(wz50000))) → GT
new_compare(Neg(Succ(wz505000)), Pos(wz5000)) → LT
new_compare(Neg(Zero), Neg(Succ(wz50000))) → new_primCmpNat0(wz50000, Zero)
new_compare(Pos(Zero), Pos(Zero)) → EQ
new_not(EQ) → new_not0
new_not(GT) → False
new_not(LT) → new_not0
new_not0 → True
new_primCmpNat0(wz505000, Zero) → GT
new_primCmpNat0(wz505000, Succ(wz50000)) → new_primCmpNat1(wz505000, wz50000)
new_primCmpNat1(Succ(wz5050000), Succ(wz500000)) → new_primCmpNat1(wz5050000, wz500000)
new_primCmpNat1(Zero, Succ(wz500000)) → LT
new_primCmpNat1(Zero, Zero) → EQ
new_primCmpNat1(Succ(wz5050000), Zero) → GT
new_primCmpNat2(Zero, wz505000) → LT
new_primCmpNat2(Succ(wz50000), wz505000) → new_primCmpNat1(wz50000, wz505000)
new_ltEs3(wz5050, wz500) → new_not(error([]))
new_ltEs2(wz5050, wz500) → new_not(error([]))
new_ltEs14(wz5050, wz500, cb, cc, cd) → new_not(error([]))
new_ltEs9(wz5050, wz500, bg) → new_not(new_compare1(wz5050, wz500, bg))
new_compare1(:%(wz50500, wz50501), :%(wz5000, wz5001), ty_Integer) → new_compare0(new_sr0(wz50500, wz5001), new_sr0(wz5000, wz50501))
new_compare1(:%(wz50500, wz50501), :%(wz5000, wz5001), ty_Int) → new_compare(new_sr(wz50500, wz5001), new_sr(wz5000, wz50501))
new_sr(Neg(wz6000), Neg(wz510)) → Pos(new_primMulNat0(wz6000, wz510))
new_sr(Pos(wz6000), Pos(wz510)) → Pos(new_primMulNat0(wz6000, wz510))
new_sr(Pos(wz6000), Neg(wz510)) → Neg(new_primMulNat0(wz6000, wz510))
new_sr(Neg(wz6000), Pos(wz510)) → Neg(new_primMulNat0(wz6000, wz510))
new_primMulNat0(Succ(wz60000), Zero) → Zero
new_primMulNat0(Zero, Succ(wz5100)) → Zero
new_primMulNat0(Succ(wz60000), Succ(wz5100)) → new_primPlusNat1(new_primMulNat0(wz60000, Succ(wz5100)), wz5100)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wz5100) → Succ(wz5100)
new_primPlusNat1(Succ(wz5120), wz5100) → Succ(Succ(new_primPlusNat0(wz5120, wz5100)))
new_primPlusNat0(Succ(wz51200), Succ(wz51000)) → Succ(Succ(new_primPlusNat0(wz51200, wz51000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Zero, Succ(wz51000)) → Succ(wz51000)
new_primPlusNat0(Succ(wz51200), Zero) → Succ(wz51200)
new_sr0(wz50500, wz5001) → error([])
new_compare0(wz5050, wz500) → error([])
new_ltEs8(wz5050, wz500) → new_not(error([]))
new_ltEs12(wz5050, wz500) → new_not(new_compare0(wz5050, wz500))
new_ltEs(wz5040, wz500, app(ty_[], bc)) → new_ltEs4(wz5040, wz500, bc)
new_ltEs(wz5040, wz500, ty_Ordering) → new_ltEs7(wz5040, wz500)
new_ltEs(wz5040, wz500, ty_@0) → new_ltEs10(wz5040, wz500)
new_ltEs(wz5040, wz500, ty_Double) → new_ltEs8(wz5040, wz500)
new_ltEs(wz5040, wz500, ty_Float) → new_ltEs3(wz5040, wz500)
new_ltEs(wz5040, wz500, app(app(ty_Either, bd), be)) → new_ltEs5(wz5040, wz500, bd, be)
new_ltEs(wz5040, wz500, ty_Bool) → new_ltEs13(wz5040, wz500)
new_ltEs(wz5040, wz500, app(app(ty_@2, bh), ca)) → new_ltEs11(wz5040, wz500, bh, ca)
new_ltEs(wz5040, wz500, ty_Int) → new_ltEs1(wz5040, wz500)
new_ltEs(wz5040, wz500, app(ty_Maybe, bf)) → new_ltEs6(wz5040, wz500, bf)
new_ltEs(wz5040, wz500, ty_Char) → new_ltEs2(wz5040, wz500)
new_ltEs(wz5040, wz500, ty_Integer) → new_ltEs12(wz5040, wz500)
new_ltEs(wz5040, wz500, app(ty_Ratio, bg)) → new_ltEs9(wz5040, wz500, bg)
new_ltEs(wz5040, wz500, app(app(app(ty_@3, cb), cc), cd)) → new_ltEs14(wz5040, wz500, cb, cc, cd)

The set Q consists of the following terms:

new_ltEs0(x0, x1, ty_Char)
new_not(GT)
new_compare1(:%(x0, x1), :%(x2, x3), ty_Integer)
new_ltEs0(x0, x1, ty_@0)
new_ltEs0(x0, x1, ty_Double)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Zero, Succ(x0))
new_compare0(x0, x1)
new_primMulNat0(Zero, Zero)
new_primPlusNat1(Zero, x0)
new_ltEs(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs(x0, x1, app(ty_Ratio, x2))
new_sr(Pos(x0), Pos(x1))
new_ltEs0(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs(x0, x1, app(app(ty_@2, x2), x3))
new_foldFM_LE0(x0, x1, x2, Branch(x3, x4, x5, x6, x7), x8, x9, x10)
new_primCmpNat0(x0, Zero)
new_ltEs10(x0, x1)
new_primPlusNat0(Succ(x0), Succ(x1))
new_ltEs0(x0, x1, ty_Integer)
new_ltEs(x0, x1, ty_Int)
new_primCmpNat0(x0, Succ(x1))
new_ltEs7(x0, x1)
new_ltEs8(x0, x1)
new_ltEs0(x0, x1, ty_Bool)
new_ltEs0(x0, x1, app(ty_Maybe, x2))
new_ltEs(x0, x1, ty_Ordering)
new_compare(Neg(Succ(x0)), Neg(x1))
new_ltEs0(x0, x1, app(app(ty_@2, x2), x3))
new_compare(Neg(Zero), Neg(Succ(x0)))
new_compare(Pos(Zero), Neg(Zero))
new_compare(Neg(Zero), Pos(Zero))
new_ltEs4(x0, x1, x2)
new_ltEs11(x0, x1, x2, x3)
new_not0
new_primPlusNat0(Zero, Zero)
new_compare(Pos(Succ(x0)), Pos(x1))
new_ltEs(x0, x1, ty_@0)
new_ltEs(x0, x1, ty_Bool)
new_ltEs0(x0, x1, ty_Ordering)
new_sr0(x0, x1)
new_primCmpNat2(Succ(x0), x1)
new_primPlusNat0(Succ(x0), Zero)
new_primCmpNat1(Succ(x0), Zero)
new_primCmpNat1(Zero, Zero)
new_ltEs3(x0, x1)
new_not(EQ)
new_ltEs(x0, x1, ty_Float)
new_compare(Neg(Zero), Neg(Zero))
new_ltEs0(x0, x1, app(ty_Ratio, x2))
new_compare(Pos(Zero), Pos(Zero))
new_primPlusNat1(Succ(x0), x1)
new_primCmpNat1(Zero, Succ(x0))
new_ltEs0(x0, x1, app(ty_[], x2))
new_ltEs1(x0, x1)
new_ltEs(x0, x1, ty_Double)
new_ltEs(x0, x1, app(ty_Maybe, x2))
new_ltEs13(x0, x1)
new_ltEs(x0, x1, ty_Integer)
new_sr(Neg(x0), Neg(x1))
new_foldFM_LE0(x0, x1, x2, EmptyFM, x3, x4, x5)
new_compare1(:%(x0, x1), :%(x2, x3), ty_Int)
new_ltEs0(x0, x1, ty_Int)
new_ltEs(x0, x1, ty_Char)
new_ltEs0(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs12(x0, x1)
new_primMulNat0(Succ(x0), Succ(x1))
new_ltEs6(x0, x1, x2)
new_compare(Pos(Zero), Pos(Succ(x0)))
new_not(LT)
new_primCmpNat2(Zero, x0)
new_ltEs(x0, x1, app(ty_[], x2))
new_primPlusNat0(Zero, Succ(x0))
new_primCmpNat1(Succ(x0), Succ(x1))
new_ltEs14(x0, x1, x2, x3, x4)
new_ltEs5(x0, x1, x2, x3)
new_compare(Neg(Succ(x0)), Pos(x1))
new_compare(Pos(Succ(x0)), Neg(x1))
new_ltEs2(x0, x1)
new_compare(Pos(Zero), Neg(Succ(x0)))
new_compare(Neg(Zero), Pos(Succ(x0)))
new_ltEs9(x0, x1, x2)
new_ltEs0(x0, x1, ty_Float)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_foldFM_LE0(x0, x1, x2, Branch(x3, x4, x5, x6, x7), x8, x9, x10)
new_foldFM_LE0(x0, x1, x2, EmptyFM, x3, x4, x5)

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ Narrow

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldFM_LE(wz498, wz500, Branch(wz5040, wz5041, wz5042, wz5043, wz5044), h, ba, bb) → new_foldFM_LE1(wz498, wz500, wz5040, wz5041, wz5042, wz5043, wz5044, new_ltEs(wz5040, wz500, ba), h, ba, bb)
new_foldFM_LE1(wz498, wz500, wz501, wz502, wz503, wz504, Branch(wz5050, wz5051, wz5052, wz5053, wz5054), True, h, ba, bb) → new_foldFM_LE(wz498, wz500, wz504, h, ba, bb)
new_foldFM_LE2(wz498, wz501, wz502, wz500, wz5050, wz5051, wz5052, wz5053, wz5054, h, ba, bb) → new_foldFM_LE1(wz498, wz500, wz5050, wz5051, wz5052, wz5053, wz5054, new_ltEs0(wz5050, wz500, ba), h, ba, bb)
new_foldFM_LE1(wz498, wz500, wz501, wz502, wz503, wz504, Branch(wz5050, wz5051, wz5052, wz5053, wz5054), True, h, ba, bb) → new_foldFM_LE2(wz498, wz501, wz502, wz500, wz5050, wz5051, wz5052, wz5053, wz5054, h, ba, bb)
new_foldFM_LE1(wz498, wz500, wz501, wz502, wz503, Branch(wz5040, wz5041, wz5042, wz5043, wz5044), wz505, False, h, ba, bb) → new_foldFM_LE1(wz498, wz500, wz5040, wz5041, wz5042, wz5043, wz5044, new_ltEs(wz5040, wz500, ba), h, ba, bb)
new_foldFM_LE1(wz498, wz500, wz501, wz502, wz503, wz504, EmptyFM, True, h, ba, bb) → new_foldFM_LE(wz498, wz500, wz504, h, ba, bb)

The TRS R consists of the following rules:

new_ltEs0(wz5050, wz500, ty_Integer) → new_ltEs12(wz5050, wz500)
new_ltEs0(wz5050, wz500, ty_Double) → new_ltEs8(wz5050, wz500)
new_ltEs0(wz5050, wz500, app(ty_Ratio, bg)) → new_ltEs9(wz5050, wz500, bg)
new_ltEs0(wz5050, wz500, app(app(app(ty_@3, cb), cc), cd)) → new_ltEs14(wz5050, wz500, cb, cc, cd)
new_ltEs0(wz5050, wz500, ty_Char) → new_ltEs2(wz5050, wz500)
new_ltEs0(wz5050, wz500, ty_Float) → new_ltEs3(wz5050, wz500)
new_ltEs0(wz5050, wz500, ty_Int) → new_ltEs1(wz5050, wz500)
new_ltEs0(wz5050, wz500, app(app(ty_Either, bd), be)) → new_ltEs5(wz5050, wz500, bd, be)
new_ltEs0(wz5050, wz500, app(app(ty_@2, bh), ca)) → new_ltEs11(wz5050, wz500, bh, ca)
new_ltEs0(wz5050, wz500, ty_@0) → new_ltEs10(wz5050, wz500)
new_ltEs0(wz5050, wz500, app(ty_[], bc)) → new_ltEs4(wz5050, wz500, bc)
new_ltEs0(wz5050, wz500, ty_Ordering) → new_ltEs7(wz5050, wz500)
new_ltEs0(wz5050, wz500, ty_Bool) → new_ltEs13(wz5050, wz500)
new_ltEs0(wz5050, wz500, app(ty_Maybe, bf)) → new_ltEs6(wz5050, wz500, bf)
new_ltEs6(wz5050, wz500, bf) → new_not(error([]))
new_ltEs13(wz5050, wz500) → new_not(error([]))
new_ltEs7(wz5050, wz500) → new_not(error([]))
new_ltEs4(wz5050, wz500, bc) → new_not(error([]))
new_ltEs10(wz5050, wz500) → new_not(error([]))
new_ltEs11(wz5050, wz500, bh, ca) → new_not(error([]))
new_ltEs5(wz5050, wz500, bd, be) → new_not(error([]))
new_ltEs1(wz5050, wz500) → new_not(new_compare(wz5050, wz500))
new_compare(Neg(Zero), Neg(Zero)) → EQ
new_compare(Pos(Zero), Neg(Zero)) → EQ
new_compare(Neg(Zero), Pos(Zero)) → EQ
new_compare(Neg(Succ(wz505000)), Neg(wz5000)) → new_primCmpNat2(wz5000, wz505000)
new_compare(Pos(Zero), Pos(Succ(wz50000))) → new_primCmpNat2(Zero, wz50000)
new_compare(Neg(Zero), Pos(Succ(wz50000))) → LT
new_compare(Pos(Succ(wz505000)), Neg(wz5000)) → GT
new_compare(Pos(Succ(wz505000)), Pos(wz5000)) → new_primCmpNat0(wz505000, wz5000)
new_compare(Pos(Zero), Neg(Succ(wz50000))) → GT
new_compare(Neg(Succ(wz505000)), Pos(wz5000)) → LT
new_compare(Neg(Zero), Neg(Succ(wz50000))) → new_primCmpNat0(wz50000, Zero)
new_compare(Pos(Zero), Pos(Zero)) → EQ
new_not(EQ) → new_not0
new_not(GT) → False
new_not(LT) → new_not0
new_not0 → True
new_primCmpNat0(wz505000, Zero) → GT
new_primCmpNat0(wz505000, Succ(wz50000)) → new_primCmpNat1(wz505000, wz50000)
new_primCmpNat1(Succ(wz5050000), Succ(wz500000)) → new_primCmpNat1(wz5050000, wz500000)
new_primCmpNat1(Zero, Succ(wz500000)) → LT
new_primCmpNat1(Zero, Zero) → EQ
new_primCmpNat1(Succ(wz5050000), Zero) → GT
new_primCmpNat2(Zero, wz505000) → LT
new_primCmpNat2(Succ(wz50000), wz505000) → new_primCmpNat1(wz50000, wz505000)
new_ltEs3(wz5050, wz500) → new_not(error([]))
new_ltEs2(wz5050, wz500) → new_not(error([]))
new_ltEs14(wz5050, wz500, cb, cc, cd) → new_not(error([]))
new_ltEs9(wz5050, wz500, bg) → new_not(new_compare1(wz5050, wz500, bg))
new_compare1(:%(wz50500, wz50501), :%(wz5000, wz5001), ty_Integer) → new_compare0(new_sr0(wz50500, wz5001), new_sr0(wz5000, wz50501))
new_compare1(:%(wz50500, wz50501), :%(wz5000, wz5001), ty_Int) → new_compare(new_sr(wz50500, wz5001), new_sr(wz5000, wz50501))
new_sr(Neg(wz6000), Neg(wz510)) → Pos(new_primMulNat0(wz6000, wz510))
new_sr(Pos(wz6000), Pos(wz510)) → Pos(new_primMulNat0(wz6000, wz510))
new_sr(Pos(wz6000), Neg(wz510)) → Neg(new_primMulNat0(wz6000, wz510))
new_sr(Neg(wz6000), Pos(wz510)) → Neg(new_primMulNat0(wz6000, wz510))
new_primMulNat0(Succ(wz60000), Zero) → Zero
new_primMulNat0(Zero, Succ(wz5100)) → Zero
new_primMulNat0(Succ(wz60000), Succ(wz5100)) → new_primPlusNat1(new_primMulNat0(wz60000, Succ(wz5100)), wz5100)
new_primMulNat0(Zero, Zero) → Zero
new_primPlusNat1(Zero, wz5100) → Succ(wz5100)
new_primPlusNat1(Succ(wz5120), wz5100) → Succ(Succ(new_primPlusNat0(wz5120, wz5100)))
new_primPlusNat0(Succ(wz51200), Succ(wz51000)) → Succ(Succ(new_primPlusNat0(wz51200, wz51000)))
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Zero, Succ(wz51000)) → Succ(wz51000)
new_primPlusNat0(Succ(wz51200), Zero) → Succ(wz51200)
new_sr0(wz50500, wz5001) → error([])
new_compare0(wz5050, wz500) → error([])
new_ltEs8(wz5050, wz500) → new_not(error([]))
new_ltEs12(wz5050, wz500) → new_not(new_compare0(wz5050, wz500))
new_ltEs(wz5040, wz500, app(ty_[], bc)) → new_ltEs4(wz5040, wz500, bc)
new_ltEs(wz5040, wz500, ty_Ordering) → new_ltEs7(wz5040, wz500)
new_ltEs(wz5040, wz500, ty_@0) → new_ltEs10(wz5040, wz500)
new_ltEs(wz5040, wz500, ty_Double) → new_ltEs8(wz5040, wz500)
new_ltEs(wz5040, wz500, ty_Float) → new_ltEs3(wz5040, wz500)
new_ltEs(wz5040, wz500, app(app(ty_Either, bd), be)) → new_ltEs5(wz5040, wz500, bd, be)
new_ltEs(wz5040, wz500, ty_Bool) → new_ltEs13(wz5040, wz500)
new_ltEs(wz5040, wz500, app(app(ty_@2, bh), ca)) → new_ltEs11(wz5040, wz500, bh, ca)
new_ltEs(wz5040, wz500, ty_Int) → new_ltEs1(wz5040, wz500)
new_ltEs(wz5040, wz500, app(ty_Maybe, bf)) → new_ltEs6(wz5040, wz500, bf)
new_ltEs(wz5040, wz500, ty_Char) → new_ltEs2(wz5040, wz500)
new_ltEs(wz5040, wz500, ty_Integer) → new_ltEs12(wz5040, wz500)
new_ltEs(wz5040, wz500, app(ty_Ratio, bg)) → new_ltEs9(wz5040, wz500, bg)
new_ltEs(wz5040, wz500, app(app(app(ty_@3, cb), cc), cd)) → new_ltEs14(wz5040, wz500, cb, cc, cd)

The set Q consists of the following terms:

new_ltEs0(x0, x1, ty_Char)
new_not(GT)
new_compare1(:%(x0, x1), :%(x2, x3), ty_Integer)
new_ltEs0(x0, x1, ty_@0)
new_ltEs0(x0, x1, ty_Double)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_primMulNat0(Succ(x0), Zero)
new_primMulNat0(Zero, Succ(x0))
new_compare0(x0, x1)
new_primMulNat0(Zero, Zero)
new_primPlusNat1(Zero, x0)
new_ltEs(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs(x0, x1, app(ty_Ratio, x2))
new_sr(Pos(x0), Pos(x1))
new_ltEs0(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_ltEs(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs(x0, x1, app(app(ty_@2, x2), x3))
new_primCmpNat0(x0, Zero)
new_ltEs10(x0, x1)
new_primPlusNat0(Succ(x0), Succ(x1))
new_ltEs0(x0, x1, ty_Integer)
new_ltEs(x0, x1, ty_Int)
new_primCmpNat0(x0, Succ(x1))
new_ltEs7(x0, x1)
new_ltEs8(x0, x1)
new_ltEs0(x0, x1, ty_Bool)
new_ltEs0(x0, x1, app(ty_Maybe, x2))
new_ltEs(x0, x1, ty_Ordering)
new_compare(Neg(Succ(x0)), Neg(x1))
new_ltEs0(x0, x1, app(app(ty_@2, x2), x3))
new_compare(Neg(Zero), Neg(Succ(x0)))
new_compare(Pos(Zero), Neg(Zero))
new_compare(Neg(Zero), Pos(Zero))
new_ltEs4(x0, x1, x2)
new_ltEs11(x0, x1, x2, x3)
new_not0
new_primPlusNat0(Zero, Zero)
new_compare(Pos(Succ(x0)), Pos(x1))
new_ltEs(x0, x1, ty_@0)
new_ltEs(x0, x1, ty_Bool)
new_ltEs0(x0, x1, ty_Ordering)
new_sr0(x0, x1)
new_primCmpNat2(Succ(x0), x1)
new_primPlusNat0(Succ(x0), Zero)
new_primCmpNat1(Succ(x0), Zero)
new_primCmpNat1(Zero, Zero)
new_ltEs3(x0, x1)
new_not(EQ)
new_ltEs(x0, x1, ty_Float)
new_compare(Neg(Zero), Neg(Zero))
new_ltEs0(x0, x1, app(ty_Ratio, x2))
new_compare(Pos(Zero), Pos(Zero))
new_primPlusNat1(Succ(x0), x1)
new_primCmpNat1(Zero, Succ(x0))
new_ltEs0(x0, x1, app(ty_[], x2))
new_ltEs1(x0, x1)
new_ltEs(x0, x1, ty_Double)
new_ltEs(x0, x1, app(ty_Maybe, x2))
new_ltEs13(x0, x1)
new_ltEs(x0, x1, ty_Integer)
new_sr(Neg(x0), Neg(x1))
new_compare1(:%(x0, x1), :%(x2, x3), ty_Int)
new_ltEs0(x0, x1, ty_Int)
new_ltEs(x0, x1, ty_Char)
new_ltEs0(x0, x1, app(app(ty_Either, x2), x3))
new_ltEs12(x0, x1)
new_primMulNat0(Succ(x0), Succ(x1))
new_ltEs6(x0, x1, x2)
new_compare(Pos(Zero), Pos(Succ(x0)))
new_not(LT)
new_primCmpNat2(Zero, x0)
new_ltEs(x0, x1, app(ty_[], x2))
new_primPlusNat0(Zero, Succ(x0))
new_primCmpNat1(Succ(x0), Succ(x1))
new_ltEs14(x0, x1, x2, x3, x4)
new_ltEs5(x0, x1, x2, x3)
new_compare(Neg(Succ(x0)), Pos(x1))
new_compare(Pos(Succ(x0)), Neg(x1))
new_ltEs2(x0, x1)
new_compare(Pos(Zero), Neg(Succ(x0)))
new_compare(Neg(Zero), Pos(Succ(x0)))
new_ltEs9(x0, x1, x2)
new_ltEs0(x0, x1, ty_Float)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_foldFM_LE1(wz498, wz500, wz501, wz502, wz503, Branch(wz5040, wz5041, wz5042, wz5043, wz5044), wz505, False, h, ba, bb) → new_foldFM_LE1(wz498, wz500, wz5040, wz5041, wz5042, wz5043, wz5044, new_ltEs(wz5040, wz500, ba), h, ba, bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 6 > 3, 6 > 4, 6 > 5, 6 > 6, 6 > 7, 9 >= 9, 10 >= 10, 11 >= 11
new_foldFM_LE1(wz498, wz500, wz501, wz502, wz503, wz504, Branch(wz5050, wz5051, wz5052, wz5053, wz5054), True, h, ba, bb) → new_foldFM_LE2(wz498, wz501, wz502, wz500, wz5050, wz5051, wz5052, wz5053, wz5054, h, ba, bb)
The graph contains the following edges 1 >= 1, 3 >= 2, 4 >= 3, 2 >= 4, 7 > 5, 7 > 6, 7 > 7, 7 > 8, 7 > 9, 9 >= 10, 10 >= 11, 11 >= 12
new_foldFM_LE(wz498, wz500, Branch(wz5040, wz5041, wz5042, wz5043, wz5044), h, ba, bb) → new_foldFM_LE1(wz498, wz500, wz5040, wz5041, wz5042, wz5043, wz5044, new_ltEs(wz5040, wz500, ba), h, ba, bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 3 > 4, 3 > 5, 3 > 6, 3 > 7, 4 >= 9, 5 >= 10, 6 >= 11
new_foldFM_LE2(wz498, wz501, wz502, wz500, wz5050, wz5051, wz5052, wz5053, wz5054, h, ba, bb) → new_foldFM_LE1(wz498, wz500, wz5050, wz5051, wz5052, wz5053, wz5054, new_ltEs0(wz5050, wz500, ba), h, ba, bb)
The graph contains the following edges 1 >= 1, 4 >= 2, 5 >= 3, 6 >= 4, 7 >= 5, 8 >= 6, 9 >= 7, 10 >= 9, 11 >= 10, 12 >= 11
new_foldFM_LE1(wz498, wz500, wz501, wz502, wz503, wz504, Branch(wz5050, wz5051, wz5052, wz5053, wz5054), True, h, ba, bb) → new_foldFM_LE(wz498, wz500, wz504, h, ba, bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 6 >= 3, 9 >= 4, 10 >= 5, 11 >= 6
new_foldFM_LE1(wz498, wz500, wz501, wz502, wz503, wz504, EmptyFM, True, h, ba, bb) → new_foldFM_LE(wz498, wz500, wz504, h, ba, bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 6 >= 3, 9 >= 4, 10 >= 5, 11 >= 6

foldFM_LE	k z fr EmptyFM	= foldFM_LE3 k z fr EmptyFM
foldFM_LE	k z fr (Branch key elt vw fm_l fm_r)	= foldFM_LE2 k z fr (Branch key elt vw fm_l fm_r)

foldFM_LE1	k z fr key elt vw fm_l fm_r True	= foldFM_LE k (k key elt (foldFM_LE k z fr fm_l)) fr fm_r
foldFM_LE1	k z fr key elt vw fm_l fm_r False	= foldFM_LE0 k z fr key elt vw fm_l fm_r otherwise